Theorem alcom 1531

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

This proof depends on syntax axioms:   <-> wb 105   A.wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108  ax-7 1501

This proof depends on definitions:  df-bi 117

This theorem is used by:  alrot3  1538  alrot4  1539  nfalt  1631  nfexd  1814  sbnf2  2041  sbcom2v  2045  sbalyz  2059  sbal1yz  2061  sbal2  2080  2eu4  2180  ralcomf  2712  gencbval  2871  unissb  3965  dfiin2g  4045  dftr5  4232  cotr  5169  cnvsym  5171  dffun2  5387  funcnveq  5444  fun11  5448