Theorem meran1

Description: A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011)

	Ref	Expression
Assertion	meran1	⊢ ( ¬ ( ¬ ( ¬ 𝜑 ∨ 𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃 ∨ 𝜏 ) ) ) ∨ ( ¬ ( ¬ 𝜃 ∨ 𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏 ∨ 𝜑 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		orc	⊢ ( ¬ 𝜑 → ( ¬ 𝜑 ∨ 𝜓 ) )
2		olc	⊢ ( 𝜓 → ( ¬ 𝜑 ∨ 𝜓 ) )
3	1 2	ja	⊢ ( ( 𝜑 → 𝜓 ) → ( ¬ 𝜑 ∨ 𝜓 ) )
4	3	imim1i	⊢ ( ( ( ¬ 𝜑 ∨ 𝜓 ) → ( 𝜒 ∨ ( 𝜃 ∨ 𝜏 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( 𝜒 ∨ ( 𝜃 ∨ 𝜏 ) ) ) )
5		pm2.24	⊢ ( 𝜃 → ( ¬ 𝜃 → 𝜑 ) )
6		idd	⊢ ( 𝜃 → ( 𝜑 → 𝜑 ) )
7	5 6	jaod	⊢ ( 𝜃 → ( ( ¬ 𝜃 ∨ 𝜑 ) → 𝜑 ) )
8	7	com12	⊢ ( ( ¬ 𝜃 ∨ 𝜑 ) → ( 𝜃 → 𝜑 ) )
9		pm1.5	⊢ ( ( ¬ ( 𝜑 → 𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃 ∨ 𝜏 ) ) ) → ( 𝜒 ∨ ( ¬ ( 𝜑 → 𝜓 ) ∨ ( 𝜃 ∨ 𝜏 ) ) ) )
10		pm2.3	⊢ ( ( ¬ ( 𝜑 → 𝜓 ) ∨ ( 𝜃 ∨ 𝜏 ) ) → ( ¬ ( 𝜑 → 𝜓 ) ∨ ( 𝜏 ∨ 𝜃 ) ) )
11		pm1.5	⊢ ( ( ¬ ( 𝜑 → 𝜓 ) ∨ ( 𝜏 ∨ 𝜃 ) ) → ( 𝜏 ∨ ( ¬ ( 𝜑 → 𝜓 ) ∨ 𝜃 ) ) )
12		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) )
13		jcn	⊢ ( 𝜃 → ( ¬ 𝜑 → ¬ ( 𝜃 → 𝜑 ) ) )
14	12 13	imim12i	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜃 ) → ( ¬ 𝜑 → ( ¬ 𝜑 → ¬ ( 𝜃 → 𝜑 ) ) ) )
15	14	pm2.43d	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜃 ) → ( ¬ 𝜑 → ¬ ( 𝜃 → 𝜑 ) ) )
16	15	con4d	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜃 ) → ( ( 𝜃 → 𝜑 ) → 𝜑 ) )
17		imor	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜃 ) ↔ ( ¬ ( 𝜑 → 𝜓 ) ∨ 𝜃 ) )
18		imor	⊢ ( ( ( 𝜃 → 𝜑 ) → 𝜑 ) ↔ ( ¬ ( 𝜃 → 𝜑 ) ∨ 𝜑 ) )
19	16 17 18	3imtr3i	⊢ ( ( ¬ ( 𝜑 → 𝜓 ) ∨ 𝜃 ) → ( ¬ ( 𝜃 → 𝜑 ) ∨ 𝜑 ) )
20	19	orim2i	⊢ ( ( 𝜏 ∨ ( ¬ ( 𝜑 → 𝜓 ) ∨ 𝜃 ) ) → ( 𝜏 ∨ ( ¬ ( 𝜃 → 𝜑 ) ∨ 𝜑 ) ) )
21		pm1.5	⊢ ( ( 𝜏 ∨ ( ¬ ( 𝜃 → 𝜑 ) ∨ 𝜑 ) ) → ( ¬ ( 𝜃 → 𝜑 ) ∨ ( 𝜏 ∨ 𝜑 ) ) )
22	10 11 20 21	4syl	⊢ ( ( ¬ ( 𝜑 → 𝜓 ) ∨ ( 𝜃 ∨ 𝜏 ) ) → ( ¬ ( 𝜃 → 𝜑 ) ∨ ( 𝜏 ∨ 𝜑 ) ) )
23	22	orim2i	⊢ ( ( 𝜒 ∨ ( ¬ ( 𝜑 → 𝜓 ) ∨ ( 𝜃 ∨ 𝜏 ) ) ) → ( 𝜒 ∨ ( ¬ ( 𝜃 → 𝜑 ) ∨ ( 𝜏 ∨ 𝜑 ) ) ) )
24		pm1.5	⊢ ( ( 𝜒 ∨ ( ¬ ( 𝜃 → 𝜑 ) ∨ ( 𝜏 ∨ 𝜑 ) ) ) → ( ¬ ( 𝜃 → 𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏 ∨ 𝜑 ) ) ) )
25	9 23 24	3syl	⊢ ( ( ¬ ( 𝜑 → 𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃 ∨ 𝜏 ) ) ) → ( ¬ ( 𝜃 → 𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏 ∨ 𝜑 ) ) ) )
26		imor	⊢ ( ( ( 𝜑 → 𝜓 ) → ( 𝜒 ∨ ( 𝜃 ∨ 𝜏 ) ) ) ↔ ( ¬ ( 𝜑 → 𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃 ∨ 𝜏 ) ) ) )
27		imor	⊢ ( ( ( 𝜃 → 𝜑 ) → ( 𝜒 ∨ ( 𝜏 ∨ 𝜑 ) ) ) ↔ ( ¬ ( 𝜃 → 𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏 ∨ 𝜑 ) ) ) )
28	25 26 27	3imtr4i	⊢ ( ( ( 𝜑 → 𝜓 ) → ( 𝜒 ∨ ( 𝜃 ∨ 𝜏 ) ) ) → ( ( 𝜃 → 𝜑 ) → ( 𝜒 ∨ ( 𝜏 ∨ 𝜑 ) ) ) )
29	4 8 28	syl2im	⊢ ( ( ( ¬ 𝜑 ∨ 𝜓 ) → ( 𝜒 ∨ ( 𝜃 ∨ 𝜏 ) ) ) → ( ( ¬ 𝜃 ∨ 𝜑 ) → ( 𝜒 ∨ ( 𝜏 ∨ 𝜑 ) ) ) )
30		imor	⊢ ( ( ( ¬ 𝜑 ∨ 𝜓 ) → ( 𝜒 ∨ ( 𝜃 ∨ 𝜏 ) ) ) ↔ ( ¬ ( ¬ 𝜑 ∨ 𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃 ∨ 𝜏 ) ) ) )
31		imor	⊢ ( ( ( ¬ 𝜃 ∨ 𝜑 ) → ( 𝜒 ∨ ( 𝜏 ∨ 𝜑 ) ) ) ↔ ( ¬ ( ¬ 𝜃 ∨ 𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏 ∨ 𝜑 ) ) ) )
32	29 30 31	3imtr3i	⊢ ( ( ¬ ( ¬ 𝜑 ∨ 𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃 ∨ 𝜏 ) ) ) → ( ¬ ( ¬ 𝜃 ∨ 𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏 ∨ 𝜑 ) ) ) )
33	32	imori	⊢ ( ¬ ( ¬ ( ¬ 𝜑 ∨ 𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃 ∨ 𝜏 ) ) ) ∨ ( ¬ ( ¬ 𝜃 ∨ 𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏 ∨ 𝜑 ) ) ) )