Metamath Proof Explorer

Theorem rp-fakeimass

Description: A special case where implication appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020)

Ref Expression
Assertion rp-fakeimass 
|- ( ( ph \/ ch ) <-> ( ( ( ph -> ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) )

Proof

Step Hyp Ref Expression
1 pm2.521g 
 |-  ( -. ( ph -> ps ) -> ( ps -> ch ) )
2 1 a1d 
 |-  ( -. ( ph -> ps ) -> ( ph -> ( ps -> ch ) ) )
3 ax-1 
 |-  ( ch -> ( ps -> ch ) )
4 3 a1d 
 |-  ( ch -> ( ph -> ( ps -> ch ) ) )
5 2 4 ja 
 |-  ( ( ( ph -> ps ) -> ch ) -> ( ph -> ( ps -> ch ) ) )
6 ax-2 
 |-  ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )
7 6 com3r 
 |-  ( ph -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ch ) ) )
8 5 7 impbid2 
 |-  ( ph -> ( ( ( ph -> ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) )
9 ax-1 
 |-  ( ch -> ( ( ph -> ps ) -> ch ) )
10 9 4 2thd 
 |-  ( ch -> ( ( ( ph -> ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) )
11 8 10 jaoi 
 |-  ( ( ph \/ ch ) -> ( ( ( ph -> ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) )
12 jarl 
 |-  ( ( ( ph -> ps ) -> ch ) -> ( -. ph -> ch ) )
13 12 orrd 
 |-  ( ( ( ph -> ps ) -> ch ) -> ( ph \/ ch ) )
14 13 a1d 
 |-  ( ( ( ph -> ps ) -> ch ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph \/ ch ) ) )
15 simplim 
 |-  ( -. ( ph -> ( ps -> ch ) ) -> ph )
16 15 orcd 
 |-  ( -. ( ph -> ( ps -> ch ) ) -> ( ph \/ ch ) )
17 16 a1i 
 |-  ( -. ( ( ph -> ps ) -> ch ) -> ( -. ( ph -> ( ps -> ch ) ) -> ( ph \/ ch ) ) )
18 14 17 bija 
 |-  ( ( ( ( ph -> ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) -> ( ph \/ ch ) )
19 11 18 impbii 
 |-  ( ( ph \/ ch ) <-> ( ( ( ph -> ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) )