Theorem alcom 1524

Description: Theorem 19.5 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
alcom	|- ( A. x A. y ph <-> A. y A. x ph )

Proof of Theorem alcom

Step	Hyp	Ref	Expression
1		ax-7 1494	. 2 |- ( A. x A. y ph -> A. y A. x ph )
2		ax-7 1494	. 2 |- ( A. y A. x ph -> A. x A. y ph )
3	1, 2	impbii 126	1 |- ( A. x A. y ph <-> A. y A. x ph )

Syntax hints:   <-> wb 105   A.wal 1393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108  ax-7 1494

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  alrot3  1531  alrot4  1532  nfalt  1624  nfexd  1807  sbnf2  2032  sbcom2v  2036  sbalyz  2050  sbal1yz  2052  sbal2  2071  2eu4  2171  ralcomf  2692  gencbval  2849  unissb  3918  dfiin2g  3998  dftr5  4185  cotr  5110  cnvsym  5112  dffun2  5328  funcnveq  5384  fun11  5388