Theorem rp-fakeoranass 44458

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 44457	. 2 ⊢ ((𝜑 → 𝜒) ↔ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑))))
2		bicom 225	. . 3 ⊢ ((((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑))) ↔ ((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜒 ∧ 𝜓) ∨ 𝜑)))
3		orcom 884	. . . . 5 ⊢ ((𝜓 ∨ 𝜑) ↔ (𝜑 ∨ 𝜓))
4	3	anbi1ci 638	. . . 4 ⊢ ((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜑 ∨ 𝜓) ∧ 𝜒))
5		orcom 884	. . . . 5 ⊢ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜑 ∨ (𝜒 ∧ 𝜓)))
6		ancom 466	. . . . . 6 ⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒))
7	6	orbi2i 926	. . . . 5 ⊢ ((𝜑 ∨ (𝜒 ∧ 𝜓)) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒)))
8	5, 7	bitri 278	. . . 4 ⊢ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒)))
9	4, 8	bibi12i 342	. . 3 ⊢ (((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜒 ∧ 𝜓) ∨ 𝜑)) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))
10	2, 9	bitri 278	. 2 ⊢ ((((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑))) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))
11	1, 10	bitri 278	1 ⊢ ((𝜑 → 𝜒) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by: (None)