NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  alcom Unicode version

Theorem alcom 1737
Description: Theorem 19.5 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
alcom

Proof of Theorem alcom
StepHypRef Expression
1 ax-7 1734 . 2
2 ax-7 1734 . 2
31, 2impbii 180 1
Colors of variables: wff setvar class
Syntax hints:   wb 176  wal 1540
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-7 1734
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  alrot3  1738  excom  1741  sbcom  2089  sbnf2  2108  sbcom2  2114  sbal2  2134  2mo  2282  2eu4  2287  ralcomf  2769  unissb  3921  dfiin2g  4000  eqpw1  4162  pw111  4170  insklem  4304  ssfin  4470  ssopr  4846  cotr  5026  cnvsym  5027  fun11  5159  dff13  5471
  Copyright terms: Public domain W3C validator