Theorem meran1 34600

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 864	. . . . . 6 ⊢ (¬ 𝜑 → (¬ 𝜑 ∨ 𝜓))
2		olc 865	. . . . . 6 ⊢ (𝜓 → (¬ 𝜑 ∨ 𝜓))
3	1, 2	ja 186	. . . . 5 ⊢ ((𝜑 → 𝜓) → (¬ 𝜑 ∨ 𝜓))
4	3	imim1i 63	. . . 4 ⊢ (((¬ 𝜑 ∨ 𝜓) → (𝜒 ∨ (𝜃 ∨ 𝜏))) → ((𝜑 → 𝜓) → (𝜒 ∨ (𝜃 ∨ 𝜏))))
5		pm2.24 124	. . . . . 6 ⊢ (𝜃 → (¬ 𝜃 → 𝜑))
6		idd 24	. . . . . 6 ⊢ (𝜃 → (𝜑 → 𝜑))
7	5, 6	jaod 856	. . . . 5 ⊢ (𝜃 → ((¬ 𝜃 ∨ 𝜑) → 𝜑))
8	7	com12 32	. . . 4 ⊢ ((¬ 𝜃 ∨ 𝜑) → (𝜃 → 𝜑))
9		pm1.5 917	. . . . . 6 ⊢ ((¬ (𝜑 → 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) → (𝜒 ∨ (¬ (𝜑 → 𝜓) ∨ (𝜃 ∨ 𝜏))))
10		pm2.3 922	. . . . . . . 8 ⊢ ((¬ (𝜑 → 𝜓) ∨ (𝜃 ∨ 𝜏)) → (¬ (𝜑 → 𝜓) ∨ (𝜏 ∨ 𝜃)))
11		pm1.5 917	. . . . . . . 8 ⊢ ((¬ (𝜑 → 𝜓) ∨ (𝜏 ∨ 𝜃)) → (𝜏 ∨ (¬ (𝜑 → 𝜓) ∨ 𝜃)))
12		pm2.21 123	. . . . . . . . . . . . 13 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
13		jcn 162	. . . . . . . . . . . . 13 ⊢ (𝜃 → (¬ 𝜑 → ¬ (𝜃 → 𝜑)))
14	12, 13	imim12i 62	. . . . . . . . . . . 12 ⊢ (((𝜑 → 𝜓) → 𝜃) → (¬ 𝜑 → (¬ 𝜑 → ¬ (𝜃 → 𝜑))))
15	14	pm2.43d 53	. . . . . . . . . . 11 ⊢ (((𝜑 → 𝜓) → 𝜃) → (¬ 𝜑 → ¬ (𝜃 → 𝜑)))
16	15	con4d 115	. . . . . . . . . 10 ⊢ (((𝜑 → 𝜓) → 𝜃) → ((𝜃 → 𝜑) → 𝜑))
17		imor 850	. . . . . . . . . 10 ⊢ (((𝜑 → 𝜓) → 𝜃) ↔ (¬ (𝜑 → 𝜓) ∨ 𝜃))
18		imor 850	. . . . . . . . . 10 ⊢ (((𝜃 → 𝜑) → 𝜑) ↔ (¬ (𝜃 → 𝜑) ∨ 𝜑))
19	16, 17, 18	3imtr3i 291	. . . . . . . . 9 ⊢ ((¬ (𝜑 → 𝜓) ∨ 𝜃) → (¬ (𝜃 → 𝜑) ∨ 𝜑))
20	19	orim2i 908	. . . . . . . 8 ⊢ ((𝜏 ∨ (¬ (𝜑 → 𝜓) ∨ 𝜃)) → (𝜏 ∨ (¬ (𝜃 → 𝜑) ∨ 𝜑)))
21		pm1.5 917	. . . . . . . 8 ⊢ ((𝜏 ∨ (¬ (𝜃 → 𝜑) ∨ 𝜑)) → (¬ (𝜃 → 𝜑) ∨ (𝜏 ∨ 𝜑)))
22	10, 11, 20, 21	4syl 19	. . . . . . 7 ⊢ ((¬ (𝜑 → 𝜓) ∨ (𝜃 ∨ 𝜏)) → (¬ (𝜃 → 𝜑) ∨ (𝜏 ∨ 𝜑)))
23	22	orim2i 908	. . . . . 6 ⊢ ((𝜒 ∨ (¬ (𝜑 → 𝜓) ∨ (𝜃 ∨ 𝜏))) → (𝜒 ∨ (¬ (𝜃 → 𝜑) ∨ (𝜏 ∨ 𝜑))))
24		pm1.5 917	. . . . . 6 ⊢ ((𝜒 ∨ (¬ (𝜃 → 𝜑) ∨ (𝜏 ∨ 𝜑))) → (¬ (𝜃 → 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))
25	9, 23, 24	3syl 18	. . . . 5 ⊢ ((¬ (𝜑 → 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) → (¬ (𝜃 → 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))
26		imor 850	. . . . 5 ⊢ (((𝜑 → 𝜓) → (𝜒 ∨ (𝜃 ∨ 𝜏))) ↔ (¬ (𝜑 → 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))))
27		imor 850	. . . . 5 ⊢ (((𝜃 → 𝜑) → (𝜒 ∨ (𝜏 ∨ 𝜑))) ↔ (¬ (𝜃 → 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))
28	25, 26, 27	3imtr4i 292	. . . 4 ⊢ (((𝜑 → 𝜓) → (𝜒 ∨ (𝜃 ∨ 𝜏))) → ((𝜃 → 𝜑) → (𝜒 ∨ (𝜏 ∨ 𝜑))))
29	4, 8, 28	syl2im 40	. . 3 ⊢ (((¬ 𝜑 ∨ 𝜓) → (𝜒 ∨ (𝜃 ∨ 𝜏))) → ((¬ 𝜃 ∨ 𝜑) → (𝜒 ∨ (𝜏 ∨ 𝜑))))
30		imor 850	. . 3 ⊢ (((¬ 𝜑 ∨ 𝜓) → (𝜒 ∨ (𝜃 ∨ 𝜏))) ↔ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))))
31		imor 850	. . 3 ⊢ (((¬ 𝜃 ∨ 𝜑) → (𝜒 ∨ (𝜏 ∨ 𝜑))) ↔ (¬ (¬ 𝜃 ∨ 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))
32	29, 30, 31	3imtr3i 291	. 2 ⊢ ((¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) → (¬ (¬ 𝜃 ∨ 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))
33	32	imori 851	1 ⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜃 ∨ 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 844

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 206  df-or 845

This theorem is referenced by:  meran2  34601  meran3  34602