Metamath Proof Explorer

Theorem axc5c4c711

Description: Proof of a theorem that can act as a sole axiom for pure predicate calculus with ax-gen as the inference rule. This proof extends the idea of axc5c711 and related theorems. (Contributed by Andrew Salmon, 14-Jul-2011)

Ref Expression
Assertion axc5c4c711 ⊢ ∀ x ∀ y ¬ ∀ x ∀ y ∀ y φ → ψ → φ → ∀ y ∀ y φ → ψ → ∀ y φ → ∀ y ψ

Proof

Step Hyp Ref Expression
1 axc4 ⊢ ∀ y ∀ y φ → ψ → ∀ y φ → ∀ y ψ
2 hbn1 ⊢ ¬ ∀ y ∀ y φ → ψ → ∀ y ¬ ∀ y ∀ y φ → ψ
3 axc7 ⊢ ¬ ∀ x ¬ ∀ x ∀ y ∀ y φ → ψ → ∀ y ∀ y φ → ψ
4 3 con1i ⊢ ¬ ∀ y ∀ y φ → ψ → ∀ x ¬ ∀ x ∀ y ∀ y φ → ψ
5 2 4 alrimih ⊢ ¬ ∀ y ∀ y φ → ψ → ∀ y ∀ x ¬ ∀ x ∀ y ∀ y φ → ψ
6 ax-11 ⊢ ∀ y ∀ x ¬ ∀ x ∀ y ∀ y φ → ψ → ∀ x ∀ y ¬ ∀ x ∀ y ∀ y φ → ψ
7 5 6 syl ⊢ ¬ ∀ y ∀ y φ → ψ → ∀ x ∀ y ¬ ∀ x ∀ y ∀ y φ → ψ
8 1 7 nsyl4 ⊢ ¬ ∀ x ∀ y ¬ ∀ x ∀ y ∀ y φ → ψ → ∀ y φ → ∀ y ψ
9 pm2.21 ⊢ ¬ φ → φ → ∀ y ψ
10 9 spsd ⊢ ¬ φ → ∀ y φ → ∀ y ψ
11 10 1 ja ⊢ φ → ∀ y ∀ y φ → ψ → ∀ y φ → ∀ y ψ
12 8 11 ja ⊢ ∀ x ∀ y ¬ ∀ x ∀ y ∀ y φ → ψ → φ → ∀ y ∀ y φ → ψ → ∀ y φ → ∀ y ψ