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

Step	Hyp	Ref	Expression
1		imp4.1	. . 3
2	1	imp4a 589	. 2
3	2	imp 429	1

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