Theorem alcom 1407

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 1377	. 2 |- ( A. x A. y ph -> A. y A. x ph )
2		ax-7 1377	. 2 |- ( A. y A. x ph -> A. x A. y ph )
3	1, 2	impbii 124	1 |- ( A. x A. y ph <-> A. y A. x ph )

Syntax hints:   <-> wb 103   A.wal 1282

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106  ax-7 1377

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  alrot3  1414  alrot4  1415  nfalt  1510  nfexd  1684  sbnf2  1898  sbcom2v  1902  sbalyz  1916  sbal1yz  1918  sbal2  1939  2eu4  2034  ralcomf  2515  gencbval  2647  unissb  3631  dfiin2g  3711  dftr5  3878  cotr  4726  cnvsym  4728  dffun2  4932  funcnveq  4982  fun11  4986