Metamath Proof Explorer


Theorem axc711to11

Description: Rederivation of ax-11 from axc711 . Note that ax-c7 and ax-11 are not used by the rederivation. (Contributed by NM, 18-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axc711to11 ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑦𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 axc711toc7 ( ¬ ∀ 𝑦 ¬ ∀ 𝑦 ¬ ∀ 𝑥𝑦 𝜑 → ¬ ∀ 𝑥𝑦 𝜑 )
2 1 con4i ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑦 ¬ ∀ 𝑦 ¬ ∀ 𝑥𝑦 𝜑 )
3 axc711 ( ¬ ∀ 𝑦 ¬ ∀ 𝑥𝑦 𝜑 → ∀ 𝑥 𝜑 )
4 3 alimi ( ∀ 𝑦 ¬ ∀ 𝑦 ¬ ∀ 𝑥𝑦 𝜑 → ∀ 𝑦𝑥 𝜑 )
5 2 4 syl ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑦𝑥 𝜑 )