Metamath Proof Explorer

Theorem ifpnim1

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

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

Proof

Step Hyp Ref Expression
1 ifpnot23c 
 |-  ( -. if- ( ph , ps , -. ph ) <-> if- ( ph , -. ps , ph ) )
2 ifpim3 
 |-  ( ( ph -> ps ) <-> if- ( ph , ps , -. ph ) )
3 1 2 xchnxbir 
 |-  ( -. ( ph -> ps ) <-> if- ( ph , -. ps , ph ) )