Theorem rp-fakeoranass 39886

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.)

Assertion

Ref	Expression
rp-fakeoranass	⊢ ((𝜑 → 𝜒) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))

Proof of Theorem rp-fakeoranass

Step	Hyp	Ref	Expression
1		rp-fakeanorass 39885	. 2 ⊢ ((𝜑 → 𝜒) ↔ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑))))
2		bicom 224	. . 3 ⊢ ((((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑))) ↔ ((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜒 ∧ 𝜓) ∨ 𝜑)))
3		orcom 866	. . . . 5 ⊢ ((𝜓 ∨ 𝜑) ↔ (𝜑 ∨ 𝜓))
4	3	anbi1ci 627	. . . 4 ⊢ ((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜑 ∨ 𝜓) ∧ 𝜒))
5		orcom 866	. . . . 5 ⊢ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜑 ∨ (𝜒 ∧ 𝜓)))
6		ancom 463	. . . . . 6 ⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒))
7	6	orbi2i 909	. . . . 5 ⊢ ((𝜑 ∨ (𝜒 ∧ 𝜓)) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒)))
8	5, 7	bitri 277	. . . 4 ⊢ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒)))
9	4, 8	bibi12i 342	. . 3 ⊢ (((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜒 ∧ 𝜓) ∨ 𝜑)) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))
10	2, 9	bitri 277	. 2 ⊢ ((((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑))) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))
11	1, 10	bitri 277	1 ⊢ ((𝜑 → 𝜒) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844

This theorem is referenced by: (None)