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 conax1
 |-  ( -. ( ph -> ps ) -> -. ps )
2 1 pm2.21d
 |-  ( -. ( ph -> ps ) -> ( ps -> ch ) )
3 2 a1d
 |-  ( -. ( ph -> ps ) -> ( ph -> ( ps -> ch ) ) )
4 ax-1
 |-  ( ch -> ( ps -> ch ) )
5 4 a1d
 |-  ( ch -> ( ph -> ( ps -> ch ) ) )
6 3 5 ja
 |-  ( ( ( ph -> ps ) -> ch ) -> ( ph -> ( ps -> ch ) ) )
7 ax-2
 |-  ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )
8 7 com3r
 |-  ( ph -> ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ch ) ) )
9 6 8 impbid2
 |-  ( ph -> ( ( ( ph -> ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) )
10 ax-1
 |-  ( ch -> ( ( ph -> ps ) -> ch ) )
11 10 5 2thd
 |-  ( ch -> ( ( ( ph -> ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) )
12 9 11 jaoi
 |-  ( ( ph \/ ch ) -> ( ( ( ph -> ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) )
13 jarl
 |-  ( ( ( ph -> ps ) -> ch ) -> ( -. ph -> ch ) )
14 13 orrd
 |-  ( ( ( ph -> ps ) -> ch ) -> ( ph \/ ch ) )
15 14 a1d
 |-  ( ( ( ph -> ps ) -> ch ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph \/ ch ) ) )
16 simplim
 |-  ( -. ( ph -> ( ps -> ch ) ) -> ph )
17 16 orcd
 |-  ( -. ( ph -> ( ps -> ch ) ) -> ( ph \/ ch ) )
18 17 a1i
 |-  ( -. ( ( ph -> ps ) -> ch ) -> ( -. ( ph -> ( ps -> ch ) ) -> ( ph \/ ch ) ) )
19 15 18 bija
 |-  ( ( ( ( ph -> ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) -> ( ph \/ ch ) )
20 12 19 impbii
 |-  ( ( ph \/ ch ) <-> ( ( ( ph -> ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) )