Metamath Proof Explorer

Theorem ifpim3

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

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

Proof

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