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 ⊢ χ → φ ↔ φ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ χ

Proof

Step Hyp Ref Expression
1 pm1.4 ⊢ φ ∨ χ → χ ∨ φ
2 1 ord ⊢ φ ∨ χ → ¬ χ → φ
3 pm4.83 ⊢ χ → φ ∧ ¬ χ → φ ↔ φ
4 3 biimpi ⊢ χ → φ ∧ ¬ χ → φ → φ
5 2 4 sylan2 ⊢ χ → φ ∧ φ ∨ χ → φ
6 5 ex ⊢ χ → φ → φ ∨ χ → φ
7 6 anim1d ⊢ χ → φ → φ ∨ χ ∧ ψ ∨ χ → φ ∧ ψ ∨ χ
8 orc ⊢ φ → φ ∨ χ
9 8 anim1i ⊢ φ ∧ ψ ∨ χ → φ ∨ χ ∧ ψ ∨ χ
10 7 9 jctir ⊢ χ → φ → φ ∨ χ ∧ ψ ∨ χ → φ ∧ ψ ∨ χ ∧ φ ∧ ψ ∨ χ → φ ∨ χ ∧ ψ ∨ χ
11 olc ⊢ χ → φ ∨ χ
12 olc ⊢ χ → ψ ∨ χ
13 11 12 jca ⊢ χ → φ ∨ χ ∧ ψ ∨ χ
14 simpl ⊢ φ ∧ ψ ∨ χ → φ
15 13 14 imim12i ⊢ φ ∨ χ ∧ ψ ∨ χ → φ ∧ ψ ∨ χ → χ → φ
16 15 adantr ⊢ φ ∨ χ ∧ ψ ∨ χ → φ ∧ ψ ∨ χ ∧ φ ∧ ψ ∨ χ → φ ∨ χ ∧ ψ ∨ χ → χ → φ
17 10 16 impbii ⊢ χ → φ ↔ φ ∨ χ ∧ ψ ∨ χ → φ ∧ ψ ∨ χ ∧ φ ∧ ψ ∨ χ → φ ∨ χ ∧ ψ ∨ χ
18 dfbi2 ⊢ φ ∨ χ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ χ ↔ φ ∨ χ ∧ ψ ∨ χ → φ ∧ ψ ∨ χ ∧ φ ∧ ψ ∨ χ → φ ∨ χ ∧ ψ ∨ χ
19 ordir ⊢ φ ∧ ψ ∨ χ ↔ φ ∨ χ ∧ ψ ∨ χ
20 19 bicomi ⊢ φ ∨ χ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ χ
21 20 bibi1i ⊢ φ ∨ χ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ χ
22 17 18 21 3bitr2i ⊢ χ → φ ↔ φ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ χ