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

Axiom ax-meredith 1474
Description: Theorem meredith 1472 restated as an axiom. This will allow us to ensure that the rederivation of ax1 1499, ax2 1500, and ax3 1501 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.) (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 setvar class
This axiom is referenced by:  merlem1  1475  merlem2  1476  merlem3  1477  merlem4  1478  merlem5  1479  merlem7  1481  merlem8  1482  merlem9  1483  merlem10  1484  merlem11  1485  merlem13  1487  luk-1  1488  luk-2  1489
  Copyright terms: Public domain W3C validator