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

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

Proof of Theorem imp4b
StepHypRef Expression
1 imp4.1 . . 3
21imp4a 589 . 2
32imp 429 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369 This theorem is referenced by:  imp43  595  pm2.61da3ne  2777  onmindif  4972  oaordex  7226  pssnn  7758  alephval3  8512  dfac5  8530  dfac2  8532  coftr  8674  zorn2lem6  8902  addcanpi  9298  mulcanpi  9299  ltmpi  9303  ltexprlem6  9440  axpre-sup  9567  bndndx  10819  dmdprdd  17030  lssssr  17599  coe1fzgsumdlem  18343  evl1gsumdlem  18392  1stcrest  19954  mdsymlem3  27324  mdsymlem6  27327  sumdmdlem  27337  mclsax  28929  mclsppslem  28943  prtlem17  30617  cvratlem  35145  paddidm  35565  pmodlem2  35571  pclfinclN  35674 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