Metamath Proof Explorer

Theorem ifpnot23

Description: Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 ianor 
 |-  ( -. ( ph /\ ps ) <-> ( -. ph \/ -. ps ) )
2 pm4.55 
 |-  ( -. ( -. ph /\ ch ) <-> ( ph \/ -. ch ) )
3 1 2 anbi12i 
 |-  ( ( -. ( ph /\ ps ) /\ -. ( -. ph /\ ch ) ) <-> ( ( -. ph \/ -. ps ) /\ ( ph \/ -. ch ) ) )
4 ioran 
 |-  ( -. ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> ( -. ( ph /\ ps ) /\ -. ( -. ph /\ ch ) ) )
5 dfifp4 
 |-  ( if- ( ph , -. ps , -. ch ) <-> ( ( -. ph \/ -. ps ) /\ ( ph \/ -. ch ) ) )
6 3 4 5 3bitr4i 
 |-  ( -. ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> if- ( ph , -. ps , -. ch ) )
7 df-ifp 
 |-  ( if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
8 6 7 xchnxbir 
 |-  ( -. if- ( ph , ps , ch ) <-> if- ( ph , -. ps , -. ch ) )