Theorem meran1 37199

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

Assertion

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

Proof of Theorem meran1

Step	Hyp	Ref	Expression
1		orc 881	. . . . . 6 ⊢ (¬ 𝜑 → (¬ 𝜑 ∨ 𝜓))
2		olc 882	. . . . . 6 ⊢ (𝜓 → (¬ 𝜑 ∨ 𝜓))
3	1, 2	ja 188	. . . . 5 ⊢ ((𝜑 → 𝜓) → (¬ 𝜑 ∨ 𝜓))
4	3	imim1i 64	. . . 4 ⊢ (((¬ 𝜑 ∨ 𝜓) → (𝜒 ∨ (𝜃 ∨ 𝜏))) → ((𝜑 → 𝜓) → (𝜒 ∨ (𝜃 ∨ 𝜏))))
5		pm2.24 125	. . . . . 6 ⊢ (𝜃 → (¬ 𝜃 → 𝜑))
6		idd 25	. . . . . 6 ⊢ (𝜃 → (𝜑 → 𝜑))
7	5, 6	jaod 873	. . . . 5 ⊢ (𝜃 → ((¬ 𝜃 ∨ 𝜑) → 𝜑))
8	7	com12 33	. . . 4 ⊢ ((¬ 𝜃 ∨ 𝜑) → (𝜃 → 𝜑))
9		pm1.5 933	. . . . . 6 ⊢ ((¬ (𝜑 → 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) → (𝜒 ∨ (¬ (𝜑 → 𝜓) ∨ (𝜃 ∨ 𝜏))))
10		pm2.3 938	. . . . . . . 8 ⊢ ((¬ (𝜑 → 𝜓) ∨ (𝜃 ∨ 𝜏)) → (¬ (𝜑 → 𝜓) ∨ (𝜏 ∨ 𝜃)))
11		pm1.5 933	. . . . . . . 8 ⊢ ((¬ (𝜑 → 𝜓) ∨ (𝜏 ∨ 𝜃)) → (𝜏 ∨ (¬ (𝜑 → 𝜓) ∨ 𝜃)))
12		pm2.21 124	. . . . . . . . . . . . 13 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
13		jcn 163	. . . . . . . . . . . . 13 ⊢ (𝜃 → (¬ 𝜑 → ¬ (𝜃 → 𝜑)))
14	12, 13	imim12i 63	. . . . . . . . . . . 12 ⊢ (((𝜑 → 𝜓) → 𝜃) → (¬ 𝜑 → (¬ 𝜑 → ¬ (𝜃 → 𝜑))))
15	14	pm2.43d 54	. . . . . . . . . . 11 ⊢ (((𝜑 → 𝜓) → 𝜃) → (¬ 𝜑 → ¬ (𝜃 → 𝜑)))
16	15	con4d 116	. . . . . . . . . 10 ⊢ (((𝜑 → 𝜓) → 𝜃) → ((𝜃 → 𝜑) → 𝜑))
17		imor 867	. . . . . . . . . 10 ⊢ (((𝜑 → 𝜓) → 𝜃) ↔ (¬ (𝜑 → 𝜓) ∨ 𝜃))
18		imor 867	. . . . . . . . . 10 ⊢ (((𝜃 → 𝜑) → 𝜑) ↔ (¬ (𝜃 → 𝜑) ∨ 𝜑))
19	16, 17, 18	3imtr3i 294	. . . . . . . . 9 ⊢ ((¬ (𝜑 → 𝜓) ∨ 𝜃) → (¬ (𝜃 → 𝜑) ∨ 𝜑))
20	19	orim2i 924	. . . . . . . 8 ⊢ ((𝜏 ∨ (¬ (𝜑 → 𝜓) ∨ 𝜃)) → (𝜏 ∨ (¬ (𝜃 → 𝜑) ∨ 𝜑)))
21		pm1.5 933	. . . . . . . 8 ⊢ ((𝜏 ∨ (¬ (𝜃 → 𝜑) ∨ 𝜑)) → (¬ (𝜃 → 𝜑) ∨ (𝜏 ∨ 𝜑)))
22	10, 11, 20, 21	4syl 20	. . . . . . 7 ⊢ ((¬ (𝜑 → 𝜓) ∨ (𝜃 ∨ 𝜏)) → (¬ (𝜃 → 𝜑) ∨ (𝜏 ∨ 𝜑)))
23	22	orim2i 924	. . . . . 6 ⊢ ((𝜒 ∨ (¬ (𝜑 → 𝜓) ∨ (𝜃 ∨ 𝜏))) → (𝜒 ∨ (¬ (𝜃 → 𝜑) ∨ (𝜏 ∨ 𝜑))))
24		pm1.5 933	. . . . . 6 ⊢ ((𝜒 ∨ (¬ (𝜃 → 𝜑) ∨ (𝜏 ∨ 𝜑))) → (¬ (𝜃 → 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))
25	9, 23, 24	3syl 19	. . . . 5 ⊢ ((¬ (𝜑 → 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) → (¬ (𝜃 → 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))
26		imor 867	. . . . 5 ⊢ (((𝜑 → 𝜓) → (𝜒 ∨ (𝜃 ∨ 𝜏))) ↔ (¬ (𝜑 → 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))))
27		imor 867	. . . . 5 ⊢ (((𝜃 → 𝜑) → (𝜒 ∨ (𝜏 ∨ 𝜑))) ↔ (¬ (𝜃 → 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))
28	25, 26, 27	3imtr4i 295	. . . 4 ⊢ (((𝜑 → 𝜓) → (𝜒 ∨ (𝜃 ∨ 𝜏))) → ((𝜃 → 𝜑) → (𝜒 ∨ (𝜏 ∨ 𝜑))))
29	4, 8, 28	syl2im 41	. . 3 ⊢ (((¬ 𝜑 ∨ 𝜓) → (𝜒 ∨ (𝜃 ∨ 𝜏))) → ((¬ 𝜃 ∨ 𝜑) → (𝜒 ∨ (𝜏 ∨ 𝜑))))
30		imor 867	. . 3 ⊢ (((¬ 𝜑 ∨ 𝜓) → (𝜒 ∨ (𝜃 ∨ 𝜏))) ↔ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))))
31		imor 867	. . 3 ⊢ (((¬ 𝜃 ∨ 𝜑) → (𝜒 ∨ (𝜏 ∨ 𝜑))) ↔ (¬ (¬ 𝜃 ∨ 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))
32	29, 30, 31	3imtr3i 294	. 2 ⊢ ((¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) → (¬ (¬ 𝜃 ∨ 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))
33	32	imori 868	1 ⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜃 ∨ 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ 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-or 862

This theorem is used by:  meran2  37200  meran3  37201