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

Theorem ax5 1695
 Description: Rederivation of axiom ax-5 1533 from the orginal version, ax-5o 1694. See ax5o 1693 for the derivation of ax-5o 1694 from ax-5 1533. This theorem should not be referenced in any proof. Instead, use ax-5 1533 above so that uses of ax-5 1533 can be more easily identified. Note: This is the same as theorem alim 1548 below. It is proved separately here so that it won't be dependent on the axioms used for alim 1548. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ax5

Proof of Theorem ax5
StepHypRef Expression
1 ax-4 1692 . . . . 5
2 ax-4 1692 . . . . 5
31, 2syl5 30 . . . 4
43ax-gen 1536 . . 3
5 ax-5o 1694 . . 3
64, 5ax-mp 10 . 2
7 ax-5o 1694 . 2
86, 7syl 17 1
 Colors of variables: wff set class Syntax hints:   wi 6  wal 1532 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10  ax-gen 1536  ax-4 1692  ax-5o 1694
 Copyright terms: Public domain W3C validator