Metamath Proof Explorer

Theorem ifpnotnotb

Description: Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 ifpnot23 
 |-  ( -. if- ( ph , ps , ch ) <-> if- ( ph , -. ps , -. ch ) )
2 1 bicomi 
 |-  ( if- ( ph , -. ps , -. ch ) <-> -. if- ( ph , ps , ch ) )