Theorem ax11-pm2 32823

Description: Proof of ax-11 2034 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2037 (PM*11.2). This proof requires that x and y be distinct. Axiom ax-11 2034 is used in the proof only through nfal 2153, nfsb 2440, sbal 2462, sb8 2424. See also ax11-pm 32819. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)

Assertion

Ref	Expression
ax11-pm2	|- ( A. x A. y ph -> A. y A. x ph )

Distinct variable group:   x, y

Allowed substitution hints:   ph( x, y)

Proof of Theorem ax11-pm2

Dummy variables z t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		2stdpc4 2354	. . . . . 6 |- ( A. x A. y ph -> [ z / x ] [ t / y ] ph )
2	1	gen2 1723	. . . . 5 |- A. t A. z ( A. x A. y ph -> [ z / x ] [ t / y ] ph )
3		nfv 1843	. . . . . . . 8 |- F/ t ph
4	3	nfal 2153	. . . . . . 7 |- F/ t A. y ph
5	4	nfal 2153	. . . . . 6 |- F/ t A. x A. y ph
6		nfv 1843	. . . . . . . 8 |- F/ z ph
7	6	nfal 2153	. . . . . . 7 |- F/ z A. y ph
8	7	nfal 2153	. . . . . 6 |- F/ z A. x A. y ph
9	5, 8	2stdpc5 32816	. . . . 5 |- ( A. t A. z ( A. x A. y ph -> [ z / x ] [ t / y ] ph ) -> ( A. x A. y ph -> A. t A. z [ z / x ] [ t / y ] ph ) )
10	2, 9	ax-mp 5	. . . 4 |- ( A. x A. y ph -> A. t A. z [ z / x ] [ t / y ] ph )
11	6	nfsb 2440	. . . . . 6 |- F/ z [ t / y ] ph
12	11	sb8 2424	. . . . 5 |- ( A. x [ t / y ] ph <-> A. z [ z / x ] [ t / y ] ph )
13	12	albii 1747	. . . 4 |- ( A. t A. x [ t / y ] ph <-> A. t A. z [ z / x ] [ t / y ] ph )
14	10, 13	sylibr 224	. . 3 |- ( A. x A. y ph -> A. t A. x [ t / y ] ph )
15		sbal 2462	. . . 4 |- ( [ t / y ] A. x ph <-> A. x [ t / y ] ph )
16	15	albii 1747	. . 3 |- ( A. t [ t / y ] A. x ph <-> A. t A. x [ t / y ] ph )
17	14, 16	sylibr 224	. 2 |- ( A. x A. y ph -> A. t [ t / y ] A. x ph )
18	3	nfal 2153	. . 3 |- F/ t A. x ph
19	18	sb8 2424	. 2 |- ( A. y A. x ph <-> A. t [ t / y ] A. x ph )
20	17, 19	sylibr 224	1 |- ( A. x A. y ph -> A. y A. x ph )

Syntax hints:   -> wi 4   A.wal 1481   [wsb 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881

This theorem is referenced by: (None)