Theorem imp31 432

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
imp3.1

Assertion

Ref	Expression
imp31

Proof of Theorem imp31

Step	Hyp	Ref	Expression
1		imp3.1	. . 3
2	1	imp 429	. 2
3	2	imp 429	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  imp41  593  imp5d  599  impl  620  anassrs  648  an31s  806  3imp  1190  3expa  1196  reusv3  4660  otiunsndisj  4758  pwssun  4791  fri  4846  ordelord  4905  tz7.7  4909  dfimafn  5922  funimass4  5924  funimass3  6003  isomin  6233  isopolem  6241  onint  6630  limsssuc  6685  tfindsg  6695  findsg  6727  suppfnss  6944  smores2  7044  tfrlem9  7073  tz7.49  7129  oecl  7206  oaordi  7214  oaass  7229  omordi  7234  odi  7247  oen0  7254  nnaordi  7286  nnmordi  7299  php3  7723  domunfican  7813  dfac5  8530  cofsmo  8670  cfcoflem  8673  zorn2lem7  8903  tskwun  9183  mulcanpi  9299  ltexprlem7  9441  sup3  10525  elnnz  10899  irradd  11235  irrmul  11236  uzsubsubfz  11736  fzo1fzo0n0  11864  elfzonelfzo  11912  uzindi  12091  ssnn0fi  12094  sqlecan  12274  swrdnd  12657  wrd2ind  12703  repswccat  12757  cshwlen  12770  cshwidxmod  12774  2cshwcshw  12793  unbenlem  14426  infpnlem1  14428  iscatd  15070  dirtr  15866  telgsums  17022  psrbaglefi  18023  psrbaglefiOLD  18024  gsummoncoe1  18346  psgndiflemA  18637  isphld  18689  gsummatr01lem3  19159  cpmatmcllem  19219  mp2pm2mplem4  19310  chfacfisf  19355  chfacfisfcpmat  19356  cayleyhamilton1  19393  tgcl  19471  neindisj2  19624  bwthOLD  19911  2ndcdisj  19957  fgcl  20379  rnelfm  20454  alexsubALTlem3  20549  usgraexmpledg  24403  usgrares1  24410  usgrafis  24415  nbgraf1olem5  24445  nbcusgra  24463  cusgrares  24472  cusgrasize  24478  usgrnloop  24565  pthdepisspth  24576  usgra2adedgspthlem2  24612  usgra2wlkspth  24621  fargshiftfva  24639  usgrcyclnl2  24641  wwlkextinj  24730  wwlkextproplem2  24742  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwwlkf1  24796  clwlkfclwwlk  24844  el2spthonot  24870  2spontn0vne  24887  eupatrl  24968  frgra3vlem1  25000  3vfriswmgralem  25004  vdgn0frgrav2  25024  vdgn1frgrav2  25026  frgrancvvdeqlemC  25039  frgrancvvdgeq  25043  frgrawopreglem5  25048  frg2woteq  25060  usg2spot2nb  25065  2spotmdisj  25068  extwwlkfablem2  25078  numclwwlkovf2ex  25086  rngoueqz  25432  mdexchi  27254  atomli  27301  mdsymlem5  27326  sumdmdlem  27337  dfimafnf  27473  mclsind  28930  dfon2lem6  29220  predpo  29264  btwnconn1lem11  29747  itg2addnc  30069  finminlem  30136  dmncan1  30473  eldioph2  30695  funressnfv  32213  dfaimafn  32250  otiunsndisjX  32301  elfz2z  32331  usgra2pthlem1  32353  initoeu1  32617  termoeu1  32624  zrtermorngc  32809  zrtermoringc  32878  snlindsntor  33072  ldepspr  33074  bnj517  33943  bnj1118  34040  lshpdisj  34712  2at0mat0  35249  llncvrlpln2  35281  lplncvrlvol2  35339  lhpexle2lem  35733  cdlemk33N  36635  cdlemk34  36636

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