Theorem rp-fakeoranass 37859

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 37858	. 2 ⊢ ((𝜑 → 𝜒) ↔ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑))))
2		bicom 212	. . 3 ⊢ ((((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑))) ↔ ((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜒 ∧ 𝜓) ∨ 𝜑)))
3		ancom 466	. . . . 5 ⊢ ((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜓 ∨ 𝜑) ∧ 𝜒))
4		orcom 402	. . . . . 6 ⊢ ((𝜓 ∨ 𝜑) ↔ (𝜑 ∨ 𝜓))
5	4	anbi1i 731	. . . . 5 ⊢ (((𝜓 ∨ 𝜑) ∧ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∧ 𝜒))
6	3, 5	bitri 264	. . . 4 ⊢ ((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜑 ∨ 𝜓) ∧ 𝜒))
7		orcom 402	. . . . 5 ⊢ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜑 ∨ (𝜒 ∧ 𝜓)))
8		ancom 466	. . . . . 6 ⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒))
9	8	orbi2i 541	. . . . 5 ⊢ ((𝜑 ∨ (𝜒 ∧ 𝜓)) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒)))
10	7, 9	bitri 264	. . . 4 ⊢ (((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒)))
11	6, 10	bibi12i 329	. . 3 ⊢ (((𝜒 ∧ (𝜓 ∨ 𝜑)) ↔ ((𝜒 ∧ 𝜓) ∨ 𝜑)) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))
12	2, 11	bitri 264	. 2 ⊢ ((((𝜒 ∧ 𝜓) ∨ 𝜑) ↔ (𝜒 ∧ (𝜓 ∨ 𝜑))) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))
13	1, 12	bitri 264	1 ⊢ ((𝜑 → 𝜒) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒))))

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384

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 197  df-or 385  df-an 386

This theorem is referenced by: (None)