Theorem axi12 2703

Description: Axiom of Quantifier Introduction (intuitionistic logic axiom ax-i12). In classical logic, this is mostly a restatement of axc9 2384 (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 2374. (Contributed by Jim Kingdon, 31-Dec-2017.) Avoid ax-11 2162. (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 2156	. . . . 5 ⊢ Ⅎ𝑧∀𝑧 𝑧 = 𝑥
2		nfa1 2156	. . . . 5 ⊢ Ⅎ𝑧∀𝑧 𝑧 = 𝑦
3	1, 2	nfor 1905	. . . 4 ⊢ Ⅎ𝑧(∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦)
4	3	19.32 2238	. . 3 ⊢ (∀𝑧((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ ((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
5		axc9 2384	. . . . . 6 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
6	5	orrd 863	. . . . 5 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (∀𝑧 𝑧 = 𝑦 ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
7	6	orri 862	. . . 4 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
8		orass 921	. . . 4 ⊢ (((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))))
9	7, 8	mpbir 231	. . 3 ⊢ ((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
10	4, 9	mpgbi 1799	. 2 ⊢ ((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
11		orass 921	. 2 ⊢ (((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))))
12	10, 11	mpbi 230	1 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 847  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2146  ax-12 2182  ax-13 2374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785

This theorem is referenced by:  axbnd  2704