Metamath Proof Explorer

Theorem rp-fakeoranass

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

Ref Expression
Assertion rp-fakeoranass ⊢ φ → χ ↔ φ ∨ ψ ∧ χ ↔ φ ∨ ψ ∧ χ

Proof

Step Hyp Ref Expression
1 rp-fakeanorass ⊢ φ → χ ↔ χ ∧ ψ ∨ φ ↔ χ ∧ ψ ∨ φ
2 bicom ⊢ χ ∧ ψ ∨ φ ↔ χ ∧ ψ ∨ φ ↔ χ ∧ ψ ∨ φ ↔ χ ∧ ψ ∨ φ
3 orcom ⊢ ψ ∨ φ ↔ φ ∨ ψ
4 3 anbi1ci ⊢ χ ∧ ψ ∨ φ ↔ φ ∨ ψ ∧ χ
5 orcom ⊢ χ ∧ ψ ∨ φ ↔ φ ∨ χ ∧ ψ
6 ancom ⊢ χ ∧ ψ ↔ ψ ∧ χ
7 6 orbi2i ⊢ φ ∨ χ ∧ ψ ↔ φ ∨ ψ ∧ χ
8 5 7 bitri ⊢ χ ∧ ψ ∨ φ ↔ φ ∨ ψ ∧ χ
9 4 8 bibi12i ⊢ χ ∧ ψ ∨ φ ↔ χ ∧ ψ ∨ φ ↔ φ ∨ ψ ∧ χ ↔ φ ∨ ψ ∧ χ
10 2 9 bitri ⊢ χ ∧ ψ ∨ φ ↔ χ ∧ ψ ∨ φ ↔ φ ∨ ψ ∧ χ ↔ φ ∨ ψ ∧ χ
11 1 10 bitri ⊢ φ → χ ↔ φ ∨ ψ ∧ χ ↔ φ ∨ ψ ∧ χ