Metamath Proof Explorer

Theorem ifpimimb

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

Ref Expression
Assertion ifpimimb 
|- ( 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 imor 
 |-  ( ( ph -> ( ps -> ch ) ) <-> ( -. ph \/ ( ps -> ch ) ) )
3 pm4.8 
 |-  ( ( ph -> -. ph ) <-> -. ph )
4 3 bicomi 
 |-  ( -. ph <-> ( ph -> -. ph ) )
5 4 orbi1i 
 |-  ( ( -. ph \/ ( ps -> ch ) ) <-> ( ( ph -> -. ph ) \/ ( ps -> ch ) ) )
6 id 
 |-  ( ph -> ph )
7 6 orci 
 |-  ( ( ph -> ph ) \/ ( th -> ch ) )
8 7 biantru 
 |-  ( ( ( ph -> -. ph ) \/ ( ps -> ch ) ) <-> ( ( ( ph -> -. ph ) \/ ( ps -> ch ) ) /\ ( ( ph -> ph ) \/ ( th -> ch ) ) ) )
9 2 5 8 3bitri 
 |-  ( ( ph -> ( ps -> ch ) ) <-> ( ( ( ph -> -. ph ) \/ ( ps -> ch ) ) /\ ( ( ph -> ph ) \/ ( th -> ch ) ) ) )
10 pm4.64 
 |-  ( ( -. ph -> ( th -> ta ) ) <-> ( ph \/ ( th -> ta ) ) )
11 pm4.81 
 |-  ( ( -. ph -> ph ) <-> ph )
12 11 bicomi 
 |-  ( ph <-> ( -. ph -> ph ) )
13 12 orbi1i 
 |-  ( ( ph \/ ( th -> ta ) ) <-> ( ( -. ph -> ph ) \/ ( th -> ta ) ) )
14 6 orci 
 |-  ( ( ph -> ph ) \/ ( ps -> ta ) )
15 14 biantrur 
 |-  ( ( ( -. ph -> ph ) \/ ( th -> ta ) ) <-> ( ( ( ph -> ph ) \/ ( ps -> ta ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) )
16 10 13 15 3bitri 
 |-  ( ( -. ph -> ( th -> ta ) ) <-> ( ( ( ph -> ph ) \/ ( ps -> ta ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) )
17 9 16 anbi12i 
 |-  ( ( ( ph -> ( ps -> ch ) ) /\ ( -. ph -> ( th -> ta ) ) ) <-> ( ( ( ( ph -> -. ph ) \/ ( ps -> ch ) ) /\ ( ( ph -> ph ) \/ ( th -> ch ) ) ) /\ ( ( ( ph -> ph ) \/ ( ps -> ta ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) ) )
18 ifpim123g 
 |-  ( ( if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) <-> ( ( ( ( ph -> -. ph ) \/ ( ps -> ch ) ) /\ ( ( ph -> ph ) \/ ( th -> ch ) ) ) /\ ( ( ( ph -> ph ) \/ ( ps -> ta ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) ) )
19 18 bicomi 
 |-  ( ( ( ( ( ph -> -. ph ) \/ ( ps -> ch ) ) /\ ( ( ph -> ph ) \/ ( th -> ch ) ) ) /\ ( ( ( ph -> ph ) \/ ( ps -> ta ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) ) <-> ( if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) )
20 1 17 19 3bitri 
 |-  ( if- ( ph , ( ps -> ch ) , ( th -> ta ) ) <-> ( if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) )