Metamath Proof Explorer

Theorem ifpimim

Description: Consequnce of implication. (Contributed by RP, 17-Apr-2020)

Ref Expression
Assertion ifpimim 
|- ( if- ( ph , ( ps -> ch ) , ( th -> ta ) ) -> ( if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) )

Proof

Step Hyp Ref Expression
1 pm2.521 
 |-  ( -. ( -. ph -> ph ) -> ( ph -> -. ph ) )
2 1 orim1i 
 |-  ( ( -. ( -. ph -> ph ) \/ ( ps -> ch ) ) -> ( ( ph -> -. ph ) \/ ( ps -> ch ) ) )
3 2 adantr 
 |-  ( ( ( -. ( -. ph -> ph ) \/ ( ps -> ch ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) -> ( ( ph -> -. ph ) \/ ( ps -> ch ) ) )
4 id 
 |-  ( ph -> ph )
5 4 orci 
 |-  ( ( ph -> ph ) \/ ( th -> ch ) )
6 5 a1i 
 |-  ( ( ( -. ( -. ph -> ph ) \/ ( ps -> ch ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) -> ( ( ph -> ph ) \/ ( th -> ch ) ) )
7 3 6 jca 
 |-  ( ( ( -. ( -. ph -> ph ) \/ ( ps -> ch ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) -> ( ( ( ph -> -. ph ) \/ ( ps -> ch ) ) /\ ( ( ph -> ph ) \/ ( th -> ch ) ) ) )
8 4 orci 
 |-  ( ( ph -> ph ) \/ ( ps -> ta ) )
9 8 a1i 
 |-  ( ( ( -. ( -. ph -> ph ) \/ ( ps -> ch ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) -> ( ( ph -> ph ) \/ ( ps -> ta ) ) )
10 simpr 
 |-  ( ( ( -. ( -. ph -> ph ) \/ ( ps -> ch ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) -> ( ( -. ph -> ph ) \/ ( th -> ta ) ) )
11 9 10 jca 
 |-  ( ( ( -. ( -. ph -> ph ) \/ ( ps -> ch ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) -> ( ( ( ph -> ph ) \/ ( ps -> ta ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) )
12 7 11 jca 
 |-  ( ( ( -. ( -. ph -> ph ) \/ ( ps -> ch ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) -> ( ( ( ( ph -> -. ph ) \/ ( ps -> ch ) ) /\ ( ( ph -> ph ) \/ ( th -> ch ) ) ) /\ ( ( ( ph -> ph ) \/ ( ps -> ta ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) ) )
13 pm4.81 
 |-  ( ( -. ph -> ph ) <-> ph )
14 13 bicomi 
 |-  ( ph <-> ( -. ph -> ph ) )
15 ifpbi1 
 |-  ( ( ph <-> ( -. ph -> ph ) ) -> ( if- ( ph , ( ps -> ch ) , ( th -> ta ) ) <-> if- ( ( -. ph -> ph ) , ( ps -> ch ) , ( th -> ta ) ) ) )
16 14 15 ax-mp 
 |-  ( if- ( ph , ( ps -> ch ) , ( th -> ta ) ) <-> if- ( ( -. ph -> ph ) , ( ps -> ch ) , ( th -> ta ) ) )
17 dfifp4 
 |-  ( if- ( ( -. ph -> ph ) , ( ps -> ch ) , ( th -> ta ) ) <-> ( ( -. ( -. ph -> ph ) \/ ( ps -> ch ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) )
18 16 17 bitri 
 |-  ( if- ( ph , ( ps -> ch ) , ( th -> ta ) ) <-> ( ( -. ( -. ph -> ph ) \/ ( ps -> ch ) ) /\ ( ( -. ph -> ph ) \/ ( th -> ta ) ) ) )
19 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 ) ) ) ) )
20 12 18 19 3imtr4i 
 |-  ( if- ( ph , ( ps -> ch ) , ( th -> ta ) ) -> ( if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) )