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 x y φ y x φ

Proof

Step Hyp Ref Expression
1 2sp x y φ φ
2 1 gen2 y x x y φ φ
3 nfa2 y x y φ
4 nfa1 x x y φ
5 3 4 2stdpc5 y x x y φ φ x y φ y x φ
6 2 5 ax-mp x y φ y x φ