MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alcom Unicode version

Theorem alcom 1752
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
StepHypRef Expression
1 ax-7 1749 . 2  |-  ( A. x A. y ph  ->  A. y A. x ph )
2 ax-7 1749 . 2  |-  ( A. y A. x ph  ->  A. x A. y ph )
31, 2impbii 181 1  |-  ( A. x A. y ph  <->  A. y A. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1549
This theorem is referenced by:  alrot3  1753  excom  1756  sbcom  2164  sbnf2  2183  sbcom2  2189  sbal2  2210  2mo  2358  2eu4  2363  ralcomf  2858  unissb  4037  dfiin2g  4116  dftr5  4297  cotr  5237  cnvsym  5239  dffun2  5455  fun11  5507  aceq1  7987  isch2  22714  dfon2lem8  25401  dford4  27037  hbexg  28498  hbexgVD  28872
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-7 1749
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator