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

Metamath Proof Explorer

Theorem axc5c711to11

Description: Rederivation of ax-11 from axc5c711 . Note that ax-c7 and ax-11 are not used by the rederivation. The use of alimi (which uses ax-c5 ) is allowed since we have already proved axc5c711toc5 . (Contributed by NM, 19-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 axc5c711toc7 ⊢ ( ¬ ∀ 𝑦 ¬ ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 𝜑 → ¬ ∀ 𝑥 ∀ 𝑦 𝜑 )
2 1 con4i ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ¬ ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 𝜑 )
3 pm2.21 ⊢ ( ¬ ∀ 𝑥 ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑥 𝜑 ) )
4 axc5c711 ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑥 𝜑 ) → 𝜑 )
5 3 4 syl ⊢ ( ¬ ∀ 𝑥 ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 𝜑 → 𝜑 )
6 5 alimi ⊢ ( ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑥 𝜑 )
7 axc5c711toc7 ⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 𝜑 )
8 6 7 nsyl4 ⊢ ( ¬ ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑥 𝜑 )
9 8 alimi ⊢ ( ∀ 𝑦 ¬ ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )
10 2 9 syl ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )