Metamath Proof Explorer

Theorem ifpim4

Description: Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020)

Ref Expression
Assertion ifpim4 
|- ( ( ph -> ps ) <-> if- ( ps , ps , -. ph ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ph /\ ps ) -> ps )
2 olc 
 |-  ( ps -> ( ph \/ ps ) )
3 ifpim23g 
 |-  ( ( ( ph -> ps ) <-> if- ( ps , ps , -. ph ) ) <-> ( ( ( ph /\ ps ) -> ps ) /\ ( ps -> ( ph \/ ps ) ) ) )
4 1 2 3 mpbir2an 
 |-  ( ( ph -> ps ) <-> if- ( ps , ps , -. ph ) )