Theorem rp-fakeanorass

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

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

Proof

Step	Hyp	Ref	Expression
1		pm1.4	⊢ ( ( 𝜑 ∨ 𝜒 ) → ( 𝜒 ∨ 𝜑 ) )
2	1	ord	⊢ ( ( 𝜑 ∨ 𝜒 ) → ( ¬ 𝜒 → 𝜑 ) )
3		pm4.83	⊢ ( ( ( 𝜒 → 𝜑 ) ∧ ( ¬ 𝜒 → 𝜑 ) ) ↔ 𝜑 )
4	3	biimpi	⊢ ( ( ( 𝜒 → 𝜑 ) ∧ ( ¬ 𝜒 → 𝜑 ) ) → 𝜑 )
5	2 4	sylan2	⊢ ( ( ( 𝜒 → 𝜑 ) ∧ ( 𝜑 ∨ 𝜒 ) ) → 𝜑 )
6	5	ex	⊢ ( ( 𝜒 → 𝜑 ) → ( ( 𝜑 ∨ 𝜒 ) → 𝜑 ) )
7	6	anim1d	⊢ ( ( 𝜒 → 𝜑 ) → ( ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) → ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ) )
8		orc	⊢ ( 𝜑 → ( 𝜑 ∨ 𝜒 ) )
9	8	anim1i	⊢ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) → ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) )
10	7 9	jctir	⊢ ( ( 𝜒 → 𝜑 ) → ( ( ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) → ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ) ∧ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) → ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) ) ) )
11		olc	⊢ ( 𝜒 → ( 𝜑 ∨ 𝜒 ) )
12		olc	⊢ ( 𝜒 → ( 𝜓 ∨ 𝜒 ) )
13	11 12	jca	⊢ ( 𝜒 → ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) )
14		simpl	⊢ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) → 𝜑 )
15	13 14	imim12i	⊢ ( ( ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) → ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ) → ( 𝜒 → 𝜑 ) )
16	15	adantr	⊢ ( ( ( ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) → ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ) ∧ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) → ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) ) ) → ( 𝜒 → 𝜑 ) )
17	10 16	impbii	⊢ ( ( 𝜒 → 𝜑 ) ↔ ( ( ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) → ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ) ∧ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) → ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) ) ) )
18		dfbi2	⊢ ( ( ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) ↔ ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ) ↔ ( ( ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) → ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ) ∧ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) → ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) ) ) )
19		ordir	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) )
20	19	bicomi	⊢ ( ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ 𝜒 ) )
21	20	bibi1i	⊢ ( ( ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) ↔ ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∨ 𝜒 ) ↔ ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ) )
22	17 18 21	3bitr2i	⊢ ( ( 𝜒 → 𝜑 ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∨ 𝜒 ) ↔ ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ) )