Theorem alcom 1501

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 1471	. 2 |- ( A. x A. y ph -> A. y A. x ph )
2		ax-7 1471	. 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 1371

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  alrot3  1508  alrot4  1509  nfalt  1601  nfexd  1784  sbnf2  2009  sbcom2v  2013  sbalyz  2027  sbal1yz  2029  sbal2  2048  2eu4  2147  ralcomf  2667  gencbval  2821  unissb  3880  dfiin2g  3960  dftr5  4146  cotr  5065  cnvsym  5067  dffun2  5282  funcnveq  5338  fun11  5342