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

Theorem ax6 1698
 Description: Rederivation of axiom ax-6 1534 from the orginal version, ax-6o 1697. See ax6o 1696 for the derivation of ax-6o 1697 from ax-6 1534. This theorem should not be referenced in any proof. Instead, use ax-6 1534 above so that uses of ax-6 1534 can be more easily identified. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ax6

Proof of Theorem ax6
StepHypRef Expression
1 ax-4 1692 . . . . 5
2 id 21 . . . . . . 7
32ax-gen 1536 . . . . . 6
4 ax-5o 1694 . . . . . 6
53, 4ax-mp 10 . . . . 5
61, 5nsyl 115 . . . 4
76ax-gen 1536 . . 3
8 ax-5o 1694 . . 3
97, 8ax-mp 10 . 2
10 ax-6o 1697 . 2
119, 10nsyl4 136 1
 Colors of variables: wff set class Syntax hints:   wn 5   wi 6  wal 1532 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1536  ax-4 1692  ax-5o 1694  ax-6o 1697
 Copyright terms: Public domain W3C validator