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 ( ( 𝜑𝜒 ) ↔ ( ( ( 𝜑𝜓 ) ∧ 𝜒 ) ↔ ( 𝜑 ∨ ( 𝜓𝜒 ) ) ) )