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 φ χ φ ψ χ φ ψ χ