Metamath Proof Explorer


Theorem ax11-pm

Description: Proof of ax-11 similar to PM's proof of alcom (PM*11.2). For a proof closer to PM's proof, see ax11-pm2 . Axiom ax-11 is used in the proof only through nfa2 . (Contributed by BJ, 15-Sep-2018) (Proof modification is discouraged.)

Ref Expression
Assertion ax11-pm ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑦𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 2sp ( ∀ 𝑥𝑦 𝜑𝜑 )
2 1 gen2 𝑦𝑥 ( ∀ 𝑥𝑦 𝜑𝜑 )
3 nfa2 𝑦𝑥𝑦 𝜑
4 nfa1 𝑥𝑥𝑦 𝜑
5 3 4 2stdpc5 ( ∀ 𝑦𝑥 ( ∀ 𝑥𝑦 𝜑𝜑 ) → ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑦𝑥 𝜑 ) )
6 2 5 ax-mp ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑦𝑥 𝜑 )