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

Theorem imp4a 589
 Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp4.1
Assertion
Ref Expression
imp4a

Proof of Theorem imp4a
StepHypRef Expression
1 imp4.1 . 2
2 impexp 446 . 2
31, 2syl6ibr 227 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369 This theorem is referenced by:  imp4b  590  imp4d  592  imp55  601  imp511  602  reuss2  3777  wefrc  4878  f1oweALT  6784  tfrlem9  7073  tz7.49  7129  oaordex  7226  dfac2  8532  zorn2lem4  8900  zorn2lem7  8903  psslinpr  9430  facwordi  12367  ndvdssub  14065  pmtrfrn  16483  elcls  19574  elcls3  19584  neibl  21004  met2ndc  21026  itgcn  22249  branmfn  27024  atcvatlem  27304  atcvat4i  27316  prtlem15  30616  cvlsupr4  35070  cvlsupr5  35071  cvlsupr6  35072  2llnneN  35133  cvrat4  35167  llnexchb2  35593  cdleme48gfv1  36262  cdlemg6e  36348  dihord6apre  36983  dihord5b  36986  dihord5apre  36989  dihglblem5apreN  37018  dihglbcpreN  37027 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 185  df-an 371
 Copyright terms: Public domain W3C validator