Metamath Proof Explorer

Theorem ifpnannanb

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

Ref Expression
Assertion ifpnannanb 
|- ( if- ( ph , ( ps -/\ ch ) , ( th -/\ ta ) ) <-> ( if- ( ph , ps , th ) -/\ if- ( ph , ch , ta ) ) )

Proof

Step Hyp Ref Expression
1 df-nan 
 |-  ( ( ps -/\ ch ) <-> -. ( ps /\ ch ) )
2 df-nan 
 |-  ( ( th -/\ ta ) <-> -. ( th /\ ta ) )
3 ifpbi23 
 |-  ( ( ( ( ps -/\ ch ) <-> -. ( ps /\ ch ) ) /\ ( ( th -/\ ta ) <-> -. ( th /\ ta ) ) ) -> ( if- ( ph , ( ps -/\ ch ) , ( th -/\ ta ) ) <-> if- ( ph , -. ( ps /\ ch ) , -. ( th /\ ta ) ) ) )
4 1 2 3 mp2an 
 |-  ( if- ( ph , ( ps -/\ ch ) , ( th -/\ ta ) ) <-> if- ( ph , -. ( ps /\ ch ) , -. ( th /\ ta ) ) )
5 ifpananb 
 |-  ( if- ( ph , ( ps /\ ch ) , ( th /\ ta ) ) <-> ( if- ( ph , ps , th ) /\ if- ( ph , ch , ta ) ) )
6 5 notbii 
 |-  ( -. if- ( ph , ( ps /\ ch ) , ( th /\ ta ) ) <-> -. ( if- ( ph , ps , th ) /\ if- ( ph , ch , ta ) ) )
7 ifpnotnotb 
 |-  ( if- ( ph , -. ( ps /\ ch ) , -. ( th /\ ta ) ) <-> -. if- ( ph , ( ps /\ ch ) , ( th /\ ta ) ) )
8 df-nan 
 |-  ( ( if- ( ph , ps , th ) -/\ if- ( ph , ch , ta ) ) <-> -. ( if- ( ph , ps , th ) /\ if- ( ph , ch , ta ) ) )
9 6 7 8 3bitr4i 
 |-  ( if- ( ph , -. ( ps /\ ch ) , -. ( th /\ ta ) ) <-> ( if- ( ph , ps , th ) -/\ if- ( ph , ch , ta ) ) )
10 4 9 bitri 
 |-  ( if- ( ph , ( ps -/\ ch ) , ( th -/\ ta ) ) <-> ( if- ( ph , ps , th ) -/\ if- ( ph , ch , ta ) ) )