Theorem alcom 1408

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  alrot3  1415  alrot4  1416  nfalt  1511  nfexd  1685  sbnf2  1899  sbcom2v  1903  sbalyz  1917  sbal1yz  1919  sbal2  1940  2eu4  2035  ralcomf  2516  gencbval  2648  unissb  3639  dfiin2g  3719  dftr5  3886  cotr  4736  cnvsym  4738  dffun2  4942  funcnveq  4993  fun11  4997