Theorem axi12 2735

Description: Axiom of Quantifier Introduction (intuitionistic logic axiom ax-i12). In classical logic, this is mostly a restatement of axc9 2416 (with one additional quantifier). But in intuitionistic logic, changing the negations and implications to disjunctions makes it stronger. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by Jim Kingdon, 31-Dec-2017.) Avoid ax-11 2194. (Revised by Wolf Lammen, 24-Apr-2023.) (New usage is discouraged.)

Assertion

Ref	Expression
axi12	⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))

Proof of Theorem axi12

Step	Hyp	Ref	Expression
1		nfa1 2188	. . . . 5 ⊢ Ⅎ𝑧∀𝑧 𝑧 = 𝑥
2		nfa1 2188	. . . . 5 ⊢ Ⅎ𝑧∀𝑧 𝑧 = 𝑦
3	1, 2	nfor 1927	. . . 4 ⊢ Ⅎ𝑧(∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦)
4	3	19.32 2271	. . 3 ⊢ (∀𝑧((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ ((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
5		axc9 2416	. . . . . 6 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
6	5	orrd 876	. . . . 5 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (∀𝑧 𝑧 = 𝑦 ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
7	6	orri 875	. . . 4 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
8		orass 934	. . . 4 ⊢ (((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))))
9	7, 8	mpbir 234	. . 3 ⊢ ((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
10	4, 9	mpgbi 1821	. 2 ⊢ ((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
11		orass 934	. 2 ⊢ (((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))))
12	10, 11	mpbi 233	1 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 860  ∀wal 1561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-10 2178  ax-12 2215  ax-13 2406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-nf 1807

This theorem is referenced by:  axbnd  2736