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

Proof of Theorem ax6
StepHypRef Expression
1 ax-4 1692 . . . . 5  |-  ( A. x  -.  A. x A. x ph  ->  -.  A. x A. x ph )
2 id 21 . . . . . . 7  |-  ( A. x ph  ->  A. x ph )
32ax-gen 1536 . . . . . 6  |-  A. x
( A. x ph  ->  A. x ph )
4 ax-5o 1694 . . . . . 6  |-  ( A. x ( A. x ph  ->  A. x ph )  ->  ( A. x ph  ->  A. x A. x ph ) )
53, 4ax-mp 10 . . . . 5  |-  ( A. x ph  ->  A. x A. x ph )
61, 5nsyl 115 . . . 4  |-  ( A. x  -.  A. x A. x ph  ->  -.  A. x ph )
76ax-gen 1536 . . 3  |-  A. x
( A. x  -.  A. x A. x ph  ->  -.  A. x ph )
8 ax-5o 1694 . . 3  |-  ( A. x ( A. x  -.  A. x A. x ph  ->  -.  A. x ph )  ->  ( A. x  -.  A. x A. x ph  ->  A. x  -.  A. x ph )
)
97, 8ax-mp 10 . 2  |-  ( A. x  -.  A. x A. x ph  ->  A. x  -.  A. x ph )
10 ax-6o 1697 . 2  |-  ( -. 
A. x  -.  A. x A. x ph  ->  A. x ph )
119, 10nsyl4 136 1  |-  ( -. 
A. x ph  ->  A. x  -.  A. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6   A.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