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

Theorem alcom 1845
Description: Theorem 19.5 of [Margaris] p. 89. (Contributed by NM, 30-Jun-1993.)
Assertion
Ref Expression
alcom

Proof of Theorem alcom
StepHypRef Expression
1 ax-11 1842 . 2
2 ax-11 1842 . 2
31, 2impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  A.wal 1393
This theorem is referenced by:  alrot3  1846  excom  1849  sbnf2  2183  sbcom2  2189  sbal1  2204  sbal2  2205  2mo2  2372  2eu4OLD  2381  ralcomf  3016  unissb  4281  dfiin2g  4363  dftr5  4548  cotrg  5383  cnvsym  5386  dffun2  5603  fun11  5658  aceq1  8519  isch2  26141  moel  27382  dfon2lem8  29222  wl-sbcom2d  30011  wl-sbalnae  30012  dford4  30971  hbexg  33329  hbexgVD  33706  bj-hbaeb  34392  bj-ralcom4  34444  elintima  37765  dfhe3  37799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-11 1842
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator