This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 φ