Metamath Proof Explorer

Theorem axc5c4c711toc4

Description: Rederivation of axc4 from axc5c4c711 . Note that only propositional calculus is required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axc5c4c711toc4 ⊢ ∀ x ∀ x φ → ψ → ∀ x φ → ∀ x ψ

Proof

Step Hyp Ref Expression
1 ax-1 ⊢ ∀ x ∀ x φ → ψ → φ → ∀ x ∀ x φ → ψ
2 ax-1 ⊢ φ → ∀ x ∀ x φ → ψ → ∀ x ∀ x ¬ ∀ x ∀ x ∀ x φ → ψ → φ → ∀ x ∀ x φ → ψ
3 axc5c4c711 ⊢ ∀ x ∀ x ¬ ∀ x ∀ x ∀ x φ → ψ → φ → ∀ x ∀ x φ → ψ → ∀ x φ → ∀ x ψ
4 1 2 3 3syl ⊢ ∀ x ∀ x φ → ψ → ∀ x φ → ∀ x ψ