Theorem rp-fakeoranass 36878

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

Assertion

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

Proof of Theorem rp-fakeoranass

Step	Hyp	Ref	Expression
1		rp-fakeanorass 36877	. 2 ⊢ ((𝜑 → 𝜒) ↔ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑))))
2		bicom 211	. . 3 ⊢ ((((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑))) ↔ ((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜒 ∧ 𝜓) ∨ 𝜑)))
3		ancom 465	. . . . 5 ⊢ ((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜓 ∨ 𝜑) ∧ 𝜒))
4		orcom 401	. . . . . 6 ⊢ ((𝜓 ∨ 𝜑) ↔ (𝜑 ∨ 𝜓))
5	4	anbi1i 727	. . . . 5 ⊢ (((𝜓 ∨ 𝜑) ∧ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∧ 𝜒))
6	3, 5	bitri 263	. . . 4 ⊢ ((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜑 ∨ 𝜓) ∧ 𝜒))
7		orcom 401	. . . . 5 ⊢ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜑 ∨ (𝜒 ∧ 𝜓)))
8		ancom 465	. . . . . 6 ⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒))
9	8	orbi2i 540	. . . . 5 ⊢ ((𝜑 ∨ (𝜒 ∧ 𝜓)) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒)))
10	7, 9	bitri 263	. . . 4 ⊢ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒)))
11	6, 10	bibi12i 328	. . 3 ⊢ (((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜒 ∧ 𝜓) ∨ 𝜑)) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))
12	2, 11	bitri 263	. 2 ⊢ ((((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑))) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))
13	1, 12	bitri 263	1 ⊢ ((𝜑 → 𝜒) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))

Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383

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 196  df-or 384  df-an 385

This theorem is referenced by: (None)