Theorem alcom 1455

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

Syntax hints:   <-> wb 104   A.wal 1330

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  alrot3  1462  alrot4  1463  nfalt  1558  nfexd  1735  sbnf2  1957  sbcom2v  1961  sbalyz  1975  sbal1yz  1977  sbal2  1998  2eu4  2093  ralcomf  2595  gencbval  2737  unissb  3774  dfiin2g  3854  dftr5  4037  cotr  4928  cnvsym  4930  dffun2  5141  funcnveq  5194  fun11  5198