Theorem axi12 2731

Description: Axiom of Quantifier Introduction (intuitionistic logic axiom ax-i12). In classical logic, this is mostly a restatement of axc9 2412 (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 2402. (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 1937	. . . 4 ⊢ Ⅎ𝑧(∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦)
4	3	19.32 2270	. . 3 ⊢ (∀𝑧((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ ((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
5		axc9 2412	. . . . . 6 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
6	5	orrd 877	. . . . 5 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (∀𝑧 𝑧 = 𝑦 ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
7	6	orri 876	. . . 4 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
8		orass 935	. . . 4 ⊢ (((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))))
9	7, 8	mpbir 234	. . 3 ⊢ ((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
10	4, 9	mpgbi 1831	. 2 ⊢ ((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
11		orass 935	. 2 ⊢ (((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))))
12	10, 11	mpbi 233	1 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2178  ax-12 2213  ax-13 2402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817

This theorem is used by:  axbnd  2732