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 ¬ x φ x ¬ x φ

Proof

Step Hyp Ref Expression
1 ax-c4 x x ¬ x x φ ¬ x φ x ¬ x x φ x ¬ x φ
2 ax-c5 x ¬ x x φ ¬ x x φ
3 ax-c4 x x φ x φ x φ x x φ
4 id x φ x φ
5 3 4 mpg x φ x x φ
6 2 5 nsyl x ¬ x x φ ¬ x φ
7 1 6 mpg x ¬ x x φ x ¬ x φ
8 ax-c7 ¬ x ¬ x x φ x φ
9 7 8 nsyl4 ¬ x φ x ¬ x φ