Metamath Proof Explorer

Theorem ifpororb

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

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

Proof

Step Hyp Ref Expression
1 dfifp2 
 |-  ( if- ( ph , ( ps \/ ch ) , ( th \/ ta ) ) <-> ( ( ph -> ( ps \/ ch ) ) /\ ( -. ph -> ( th \/ ta ) ) ) )
2 df-or 
 |-  ( ( ps \/ ch ) <-> ( -. ps -> ch ) )
3 2 imbi2i 
 |-  ( ( ph -> ( ps \/ ch ) ) <-> ( ph -> ( -. ps -> ch ) ) )
4 df-or 
 |-  ( ( th \/ ta ) <-> ( -. th -> ta ) )
5 4 imbi2i 
 |-  ( ( -. ph -> ( th \/ ta ) ) <-> ( -. ph -> ( -. th -> ta ) ) )
6 3 5 anbi12i 
 |-  ( ( ( ph -> ( ps \/ ch ) ) /\ ( -. ph -> ( th \/ ta ) ) ) <-> ( ( ph -> ( -. ps -> ch ) ) /\ ( -. ph -> ( -. th -> ta ) ) ) )
7 ifpimimb 
 |-  ( if- ( ph , ( -. ps -> ch ) , ( -. th -> ta ) ) <-> ( if- ( ph , -. ps , -. th ) -> if- ( ph , ch , ta ) ) )
8 dfifp2 
 |-  ( if- ( ph , ( -. ps -> ch ) , ( -. th -> ta ) ) <-> ( ( ph -> ( -. ps -> ch ) ) /\ ( -. ph -> ( -. th -> ta ) ) ) )
9 imor 
 |-  ( ( if- ( ph , -. ps , -. th ) -> if- ( ph , ch , ta ) ) <-> ( -. if- ( ph , -. ps , -. th ) \/ if- ( ph , ch , ta ) ) )
10 ifpnot23d 
 |-  ( -. if- ( ph , -. ps , -. th ) <-> if- ( ph , ps , th ) )
11 10 orbi1i 
 |-  ( ( -. if- ( ph , -. ps , -. th ) \/ if- ( ph , ch , ta ) ) <-> ( if- ( ph , ps , th ) \/ if- ( ph , ch , ta ) ) )
12 9 11 bitri 
 |-  ( ( if- ( ph , -. ps , -. th ) -> if- ( ph , ch , ta ) ) <-> ( if- ( ph , ps , th ) \/ if- ( ph , ch , ta ) ) )
13 7 8 12 3bitr3i 
 |-  ( ( ( ph -> ( -. ps -> ch ) ) /\ ( -. ph -> ( -. th -> ta ) ) ) <-> ( if- ( ph , ps , th ) \/ if- ( ph , ch , ta ) ) )
14 1 6 13 3bitri 
 |-  ( if- ( ph , ( ps \/ ch ) , ( th \/ ta ) ) <-> ( if- ( ph , ps , th ) \/ if- ( ph , ch , ta ) ) )