Metamath Proof Explorer

Theorem axc7

Description: Show that the original axiom ax-c7 can be derived from ax-10 ( hbn1 ) , sp and propositional calculus. See ax10fromc7 for the rederivation of ax-10 from ax-c7 .

Normally, axc7 should be used rather than ax-c7 , except by theorems specifically studying the latter's properties. (Contributed by NM, 21-May-2008)

Ref Expression
Assertion axc7 ¬ x ¬ x φ φ


Step Hyp Ref Expression
1 sp x φ φ
2 hbn1 ¬ x φ x ¬ x φ
3 1 2 nsyl4 ¬ x ¬ x φ φ