Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-meredith Structured version   Unicode version

Axiom ax-meredith 1415
 Description: Theorem meredith 1413 restated as an axiom. This will allow us to ensure that the rederivation of ax1 1440, ax2 1441, and ax3 1442 below depend only on Meredith's sole axiom and not accidentally on a previous theorem above. Outside of this section, we will not make use of this axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ax-meredith

Detailed syntax breakdown of Axiom ax-meredith
StepHypRef Expression
1 wph . . . . . 6
2 wps . . . . . 6
31, 2wi 4 . . . . 5
4 wch . . . . . . 7
54wn 3 . . . . . 6
6 wth . . . . . . 7
76wn 3 . . . . . 6
85, 7wi 4 . . . . 5
93, 8wi 4 . . . 4
109, 4wi 4 . . 3
11 wta . . 3
1210, 11wi 4 . 2
1311, 1wi 4 . . 3
146, 1wi 4 . . 3
1513, 14wi 4 . 2
1612, 15wi 4 1
 Colors of variables: wff set class This axiom is referenced by:  merlem1  1416  merlem2  1417  merlem3  1418  merlem4  1419  merlem5  1420  merlem7  1422  merlem8  1423  merlem9  1424  merlem10  1425  merlem11  1426  merlem13  1428  luk-1  1429  luk-2  1430
 Copyright terms: Public domain W3C validator