Theorem axi12

Description: Axiom of Quantifier Introduction (intuitionistic logic axiom ax-i12). In classical logic, this is mostly a restatement of axc9 (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 . (Contributed by Jim Kingdon, 31-Dec-2017) Avoid ax-11 . (Revised by Wolf Lammen, 24-Apr-2023) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nfa1	⊢ Ⅎ 𝑧 ∀ 𝑧 𝑧 = 𝑥
2		nfa1	⊢ Ⅎ 𝑧 ∀ 𝑧 𝑧 = 𝑦
3	1 2	nfor	⊢ Ⅎ 𝑧 ( ∀ 𝑧 𝑧 = 𝑥 ∨ ∀ 𝑧 𝑧 = 𝑦 )
4	3	19.32	⊢ ( ∀ 𝑧 ( ( ∀ 𝑧 𝑧 = 𝑥 ∨ ∀ 𝑧 𝑧 = 𝑦 ) ∨ ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) ) ↔ ( ( ∀ 𝑧 𝑧 = 𝑥 ∨ ∀ 𝑧 𝑧 = 𝑦 ) ∨ ∀ 𝑧 ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) ) )
5		axc9	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) ) )
6	5	orrd	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑧 𝑧 = 𝑦 ∨ ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) ) )
7	6	orri	⊢ ( ∀ 𝑧 𝑧 = 𝑥 ∨ ( ∀ 𝑧 𝑧 = 𝑦 ∨ ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) ) )
8		orass	⊢ ( ( ( ∀ 𝑧 𝑧 = 𝑥 ∨ ∀ 𝑧 𝑧 = 𝑦 ) ∨ ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) ) ↔ ( ∀ 𝑧 𝑧 = 𝑥 ∨ ( ∀ 𝑧 𝑧 = 𝑦 ∨ ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) ) ) )
9	7 8	mpbir	⊢ ( ( ∀ 𝑧 𝑧 = 𝑥 ∨ ∀ 𝑧 𝑧 = 𝑦 ) ∨ ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) )
10	4 9	mpgbi	⊢ ( ( ∀ 𝑧 𝑧 = 𝑥 ∨ ∀ 𝑧 𝑧 = 𝑦 ) ∨ ∀ 𝑧 ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) )
11		orass	⊢ ( ( ( ∀ 𝑧 𝑧 = 𝑥 ∨ ∀ 𝑧 𝑧 = 𝑦 ) ∨ ∀ 𝑧 ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) ) ↔ ( ∀ 𝑧 𝑧 = 𝑥 ∨ ( ∀ 𝑧 𝑧 = 𝑦 ∨ ∀ 𝑧 ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) ) ) )
12	10 11	mpbi	⊢ ( ∀ 𝑧 𝑧 = 𝑥 ∨ ( ∀ 𝑧 𝑧 = 𝑦 ∨ ∀ 𝑧 ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) ) )