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 | |- ( A. x A. y ph -> A. y A. x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2sp | |- ( A. x A. y ph -> ph ) |
|
| 2 | 1 | gen2 | |- A. y A. x ( A. x A. y ph -> ph ) |
| 3 | nfa2 | |- F/ y A. x A. y ph |
|
| 4 | nfa1 | |- F/ x A. x A. y ph |
|
| 5 | 3 4 | 2stdpc5 | |- ( A. y A. x ( A. x A. y ph -> ph ) -> ( A. x A. y ph -> A. y A. x ph ) ) |
| 6 | 2 5 | ax-mp | |- ( A. x A. y ph -> A. y A. x ph ) |