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

Theorem alcom 1711
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 1708 . 2  |-  ( A. x A. y ph  ->  A. y A. x ph )
2 ax-7 1708 . 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 1527
This theorem is referenced by:  alrot3  1712  sbcom  2029  sbnf2  2047  sbcom2  2053  sbal2  2073  2mo  2221  2eu4  2226  ralcomf  2698  unissb  3857  dfiin2g  3936  dftr5  4116  cotr  5055  cnvsym  5057  dffun2  5265  fun11  5315  aceq1  7744  isch2  21803  dfon2lem8  24146  dford4  27122  hbexg  28322  hbexgVD  28682
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-7 1708
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator