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ψ