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

Theorem alcom 1723
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 1720 . 2  |-  ( A. x A. y ph  ->  A. y A. x ph )
2 ax-7 1720 . 2  |-  ( A. y A. x ph  ->  A. x A. y ph )
31, 2impbii 180 1  |-  ( A. x A. y ph  <->  A. y A. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1530
This theorem is referenced by:  alrot3  1724  sbcom  2042  sbnf2  2060  sbcom2  2066  sbal2  2086  2mo  2234  2eu4  2239  ralcomf  2711  unissb  3873  dfiin2g  3952  dftr5  4132  cotr  5071  cnvsym  5073  dffun2  5281  fun11  5331  aceq1  7760  isch2  21819  dfon2lem8  24217  dford4  27225  hbexg  28621  hbexgVD  28998
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-7 1720
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator