Theorem alcom 1492

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  alrot3  1499  alrot4  1500  nfalt  1592  nfexd  1775  sbnf2  2000  sbcom2v  2004  sbalyz  2018  sbal1yz  2020  sbal2  2039  2eu4  2138  ralcomf  2658  gencbval  2812  unissb  3870  dfiin2g  3950  dftr5  4135  cotr  5052  cnvsym  5054  dffun2  5269  funcnveq  5322  fun11  5326