Metamath Proof Explorer

Theorem ifpnim2

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

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

Proof

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