ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax4 Unicode version

Theorem ax4 1423
Description: Theorem showing that ax-4 1392 can be derived from ax-5 1336, ax-gen 1339, ax-8 1387, ax-9 1418, ax-11 1389, and ax-17 1402 and is therefore redundant in a system including these axioms. The proof uses ideas from the proof of Lemma 21 of [Monk2] p. 114.

This theorem should not be referenced in any proof. Instead, we will use ax-4 1392 below so that explicit uses of ax-4 1392 can be more easily identified. In particular, this will more cleanly separate out the theorems of "pure" predicate calculus that don't involve equality or distinct variables. A beginner may wish to accept ax-4 1392 a priori, so that the proof of this theorem (ax4 1423), which involves equality as well as the distinct variable requirements of ax-17 1402, can be put off until those axioms are studied.

Note: All predicate calculus axioms introduced from this point forward are redundant. Immediately before their introduction, we prove them from earlier axioms to demonstrate their redundancy. Specifically, redundant axioms ax-4 1392, ax-5o 1425, ax-6o 1428, ax-9o 1558, ax-10o 1576, ax-11o 1654, ax-15 1807, and ax-16 1644 are proved by theorems ax4 1423, ax5o 1424, ax6o 1427, ax9o 1557, ax10o 1575, ax11o 1653, ax15 1806, and ax16 1643. Except for the ones suffixed with o (ax-5o 1425 etc.), we never reference those theorems directly. Instead, we use the axiom version that immediately follows it. This allow us to better isolate the uses of the redundant axioms for easier study of subsystems containing them.

(The proof was shortened by Scott Fenton, 24-Jan-2011.)

Assertion
Ref Expression
ax4

Proof of Theorem ax4
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ax-9 1418 . 2
2 ax-9 1418 . . . . . . . . . 10
3 ax-8 1387 . . . . . . . . . . . . . 14
43pm2.43i 42 . . . . . . . . . . . . 13
54con3i 543 . . . . . . . . . . . 12
65ax-gen 1339 . . . . . . . . . . 11
7 ax-17 1402 . . . . . . . . . . 11
8 ax-5 1336 . . . . . . . . . . 11
96, 7, 8mpsyl 58 . . . . . . . . . 10
102, 9mt3 724 . . . . . . . . 9
11 ax-8 1387 . . . . . . . . 9
1210, 11mpi 15 . . . . . . . 8
13 ax-17 1402 . . . . . . . 8
14 ax-11 1389 . . . . . . . 8
1512, 13, 14syl2im 33 . . . . . . 7
16 con2 551 . . . . . . . . . . 11
1716ax-gen 1339 . . . . . . . . . 10
18 ax-5 1336 . . . . . . . . . 10
1917, 18ax-mp 8 . . . . . . . . 9
20 ax-5 1336 . . . . . . . . 9
2119, 20syl 14 . . . . . . . 8
222, 21mtoi 569 . . . . . . 7
2315, 22syl6 28 . . . . . 6
2423con4d 715 . . . . 5
2524con3i 543 . . . 4
2625ax-gen 1339 . . 3
27 ax-17 1402 . . 3
28 ax-5 1336 . . 3
2926, 27, 28mpsyl 58 . 2
301, 29mt3 724 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4  wal 1335
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-ia1 98  ax-ia2 99  ax-ia3 100  ax-in1 527  ax-in2 528  ax-5 1336  ax-gen 1339  ax-ie2 1376  ax-8 1387  ax-11 1389  ax-17 1402  ax-i9 1417
This theorem depends on definitions:  df-bi 109  df-tru 1313  df-fal 1314
  Copyright terms: Public domain W3C validator