Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > axi12 | Structured version Visualization version GIF version |
Description: Axiom of Quantifier Introduction (intuitionistic logic axiom ax-i12). In classical logic, this is mostly a restatement of axc9 2383 (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 2373. (Contributed by Jim Kingdon, 31-Dec-2017.) Avoid ax-11 2160. (Revised by Wolf Lammen, 24-Apr-2023.) (New usage is discouraged.) |
Ref | Expression |
---|---|
axi12 | ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfa1 2154 | . . . . 5 ⊢ Ⅎ𝑧∀𝑧 𝑧 = 𝑥 | |
2 | nfa1 2154 | . . . . 5 ⊢ Ⅎ𝑧∀𝑧 𝑧 = 𝑦 | |
3 | 1, 2 | nfor 1912 | . . . 4 ⊢ Ⅎ𝑧(∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) |
4 | 3 | 19.32 2233 | . . 3 ⊢ (∀𝑧((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ ((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
5 | axc9 2383 | . . . . . 6 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) | |
6 | 5 | orrd 863 | . . . . 5 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (∀𝑧 𝑧 = 𝑦 ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
7 | 6 | orri 862 | . . . 4 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
8 | orass 922 | . . . 4 ⊢ (((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))) | |
9 | 7, 8 | mpbir 234 | . . 3 ⊢ ((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
10 | 4, 9 | mpgbi 1806 | . 2 ⊢ ((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
11 | orass 922 | . 2 ⊢ (((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))) | |
12 | 10, 11 | mpbi 233 | 1 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 847 ∀wal 1541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-10 2143 ax-12 2177 ax-13 2373 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-nf 1792 |
This theorem is referenced by: axbnd 2709 |
Copyright terms: Public domain | W3C validator |