Metamath Proof Explorer

Theorem ifpananb

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

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

Proof

Step Hyp Ref Expression
1 anor 
 |-  ( ( ps /\ ch ) <-> -. ( -. ps \/ -. ch ) )
2 anor 
 |-  ( ( 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 ifpororb 
 |-  ( if- ( ph , ( -. ps \/ -. ch ) , ( -. th \/ -. ta ) ) <-> ( if- ( ph , -. ps , -. th ) \/ if- ( ph , -. ch , -. ta ) ) )
6 ifpnotnotb 
 |-  ( if- ( ph , -. ps , -. th ) <-> -. if- ( ph , ps , th ) )
7 ifpnotnotb 
 |-  ( if- ( ph , -. ch , -. ta ) <-> -. if- ( ph , ch , ta ) )
8 6 7 orbi12i 
 |-  ( ( if- ( ph , -. ps , -. th ) \/ if- ( ph , -. ch , -. ta ) ) <-> ( -. if- ( ph , ps , th ) \/ -. if- ( ph , ch , ta ) ) )
9 5 8 bitri 
 |-  ( if- ( ph , ( -. ps \/ -. ch ) , ( -. th \/ -. ta ) ) <-> ( -. if- ( ph , ps , th ) \/ -. if- ( ph , ch , ta ) ) )
10 9 notbii 
 |-  ( -. if- ( ph , ( -. ps \/ -. ch ) , ( -. th \/ -. ta ) ) <-> -. ( -. if- ( ph , ps , th ) \/ -. if- ( ph , ch , ta ) ) )
11 ifpnotnotb 
 |-  ( if- ( ph , -. ( -. ps \/ -. ch ) , -. ( -. th \/ -. ta ) ) <-> -. if- ( ph , ( -. ps \/ -. ch ) , ( -. th \/ -. ta ) ) )
12 anor 
 |-  ( ( if- ( ph , ps , th ) /\ if- ( ph , ch , ta ) ) <-> -. ( -. if- ( ph , ps , th ) \/ -. if- ( ph , ch , ta ) ) )
13 10 11 12 3bitr4i 
 |-  ( if- ( ph , -. ( -. ps \/ -. ch ) , -. ( -. th \/ -. ta ) ) <-> ( if- ( ph , ps , th ) /\ if- ( ph , ch , ta ) ) )
14 4 13 bitri 
 |-  ( if- ( ph , ( ps /\ ch ) , ( th /\ ta ) ) <-> ( if- ( ph , ps , th ) /\ if- ( ph , ch , ta ) ) )