Metamath Proof Explorer

Theorem ax10fromc7

Description: Rederivation of Axiom ax-10 from ax-c7 , ax-c4 , ax-c5 , ax-gen and propositional calculus. See axc7 for the derivation of ax-c7 from ax-10 . (Contributed by NM, 23-May-2008) (Proof modification is discouraged.) Use ax-10 instead. (New usage is discouraged.)

Ref Expression
Assertion ax10fromc7 
|- ( -. A. x ph -> A. x -. A. x ph )

Proof

Step Hyp Ref Expression
1 ax-c4 
 |-  ( A. x ( A. x -. A. x A. x ph -> -. A. x ph ) -> ( A. x -. A. x A. x ph -> A. x -. A. x ph ) )
2 ax-c5 
 |-  ( A. x -. A. x A. x ph -> -. A. x A. x ph )
3 ax-c4 
 |-  ( A. x ( A. x ph -> A. x ph ) -> ( A. x ph -> A. x A. x ph ) )
4 id 
 |-  ( A. x ph -> A. x ph )
5 3 4 mpg 
 |-  ( A. x ph -> A. x A. x ph )
6 2 5 nsyl 
 |-  ( A. x -. A. x A. x ph -> -. A. x ph )
7 1 6 mpg 
 |-  ( A. x -. A. x A. x ph -> A. x -. A. x ph )
8 ax-c7 
 |-  ( -. A. x -. A. x A. x ph -> A. x ph )
9 7 8 nsyl4 
 |-  ( -. A. x ph -> A. x -. A. x ph )