MPE Home 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  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )

Proof of Theorem ax5
StepHypRef Expression
1 ax-4 1692 . . . . 5  |-  ( A. x ph  ->  ph )
2 ax-4 1692 . . . . 5  |-  ( A. x ( ph  ->  ps )  ->  ( ph  ->  ps ) )
31, 2syl5 30 . . . 4  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  ps )
)
43ax-gen 1536 . . 3  |-  A. x
( A. x (
ph  ->  ps )  -> 
( A. x ph  ->  ps ) )
5 ax-5o 1694 . . 3  |-  ( A. x ( A. x
( ph  ->  ps )  ->  ( A. x ph  ->  ps ) )  -> 
( A. x (
ph  ->  ps )  ->  A. x ( A. x ph  ->  ps ) ) )
64, 5ax-mp 10 . 2  |-  ( A. x ( ph  ->  ps )  ->  A. x
( A. x ph  ->  ps ) )
7 ax-5o 1694 . 2  |-  ( A. x ( A. x ph  ->  ps )  -> 
( A. x ph  ->  A. x ps )
)
86, 7syl 17 1  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.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