Metamath Proof Explorer

Theorem rp-fakeanorass

Description: A special case where a mixture of and and or appears to conform to a mixed associative law. (Contributed by RP, 26-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 pm1.4 
 |-  ( ( ph \/ ch ) -> ( ch \/ ph ) )
2 1 ord 
 |-  ( ( ph \/ ch ) -> ( -. ch -> ph ) )
3 pm4.83 
 |-  ( ( ( ch -> ph ) /\ ( -. ch -> ph ) ) <-> ph )
4 3 biimpi 
 |-  ( ( ( ch -> ph ) /\ ( -. ch -> ph ) ) -> ph )
5 2 4 sylan2 
 |-  ( ( ( ch -> ph ) /\ ( ph \/ ch ) ) -> ph )
6 5 ex 
 |-  ( ( ch -> ph ) -> ( ( ph \/ ch ) -> ph ) )
7 6 anim1d 
 |-  ( ( ch -> ph ) -> ( ( ( ph \/ ch ) /\ ( ps \/ ch ) ) -> ( ph /\ ( ps \/ ch ) ) ) )
8 orc 
 |-  ( ph -> ( ph \/ ch ) )
9 8 anim1i 
 |-  ( ( ph /\ ( ps \/ ch ) ) -> ( ( ph \/ ch ) /\ ( ps \/ ch ) ) )
10 7 9 jctir 
 |-  ( ( ch -> ph ) -> ( ( ( ( ph \/ ch ) /\ ( ps \/ ch ) ) -> ( ph /\ ( ps \/ ch ) ) ) /\ ( ( ph /\ ( ps \/ ch ) ) -> ( ( ph \/ ch ) /\ ( ps \/ ch ) ) ) ) )
11 olc 
 |-  ( ch -> ( ph \/ ch ) )
12 olc 
 |-  ( ch -> ( ps \/ ch ) )
13 11 12 jca 
 |-  ( ch -> ( ( ph \/ ch ) /\ ( ps \/ ch ) ) )
14 simpl 
 |-  ( ( ph /\ ( ps \/ ch ) ) -> ph )
15 13 14 imim12i 
 |-  ( ( ( ( ph \/ ch ) /\ ( ps \/ ch ) ) -> ( ph /\ ( ps \/ ch ) ) ) -> ( ch -> ph ) )
16 15 adantr 
 |-  ( ( ( ( ( ph \/ ch ) /\ ( ps \/ ch ) ) -> ( ph /\ ( ps \/ ch ) ) ) /\ ( ( ph /\ ( ps \/ ch ) ) -> ( ( ph \/ ch ) /\ ( ps \/ ch ) ) ) ) -> ( ch -> ph ) )
17 10 16 impbii 
 |-  ( ( ch -> ph ) <-> ( ( ( ( ph \/ ch ) /\ ( ps \/ ch ) ) -> ( ph /\ ( ps \/ ch ) ) ) /\ ( ( ph /\ ( ps \/ ch ) ) -> ( ( ph \/ ch ) /\ ( ps \/ ch ) ) ) ) )
18 dfbi2 
 |-  ( ( ( ( ph \/ ch ) /\ ( ps \/ ch ) ) <-> ( ph /\ ( ps \/ ch ) ) ) <-> ( ( ( ( ph \/ ch ) /\ ( ps \/ ch ) ) -> ( ph /\ ( ps \/ ch ) ) ) /\ ( ( ph /\ ( ps \/ ch ) ) -> ( ( ph \/ ch ) /\ ( ps \/ ch ) ) ) ) )
19 ordir 
 |-  ( ( ( ph /\ ps ) \/ ch ) <-> ( ( ph \/ ch ) /\ ( ps \/ ch ) ) )
20 19 bicomi 
 |-  ( ( ( ph \/ ch ) /\ ( ps \/ ch ) ) <-> ( ( ph /\ ps ) \/ ch ) )
21 20 bibi1i 
 |-  ( ( ( ( ph \/ ch ) /\ ( ps \/ ch ) ) <-> ( ph /\ ( ps \/ ch ) ) ) <-> ( ( ( ph /\ ps ) \/ ch ) <-> ( ph /\ ( ps \/ ch ) ) ) )
22 17 18 21 3bitr2i 
 |-  ( ( ch -> ph ) <-> ( ( ( ph /\ ps ) \/ ch ) <-> ( ph /\ ( ps \/ ch ) ) ) )