Theorem imp32 433

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

Hypothesis

Ref	Expression
imp3.1

Assertion

Ref	Expression
imp32

Proof of Theorem imp32

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

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  imp42  594  impr  619  anasss  647  an13s  803  3expb  1197  reuss2  3777  reupick  3781  po2nr  4818  tz7.7  4909  ordtr2  4927  fvmptt  5971  fliftfund  6211  isomin  6233  f1ocnv2d  6526  onint  6630  tz7.48lem  7125  oalimcl  7228  oaass  7229  omass  7248  omabs  7315  finsschain  7847  infxpenlem  8412  axcc3  8839  zorn2lem7  8903  addclpi  9291  addnidpi  9300  genpnnp  9404  genpnmax  9406  mulclprlem  9418  dedekindle  9766  prodgt0  10412  ltsubrp  11280  ltaddrp  11281  swrdccatin1  12708  swrdccat3  12717  infpnlem1  14428  iscatd  15070  imasmnd2  15957  imasgrp2  16185  imasring  17268  mplcoe5lem  18130  dmatmul  18999  scmatmulcl  19020  scmatsgrp1  19024  smatvscl  19026  cpmatacl  19217  cpmatmcllem  19219  0ntr  19572  clsndisj  19576  innei  19626  islpi  19650  tgcnp  19754  haust1  19853  alexsublem  20544  alexsubb  20546  isxmetd  20829  axcontlem4  24270  wwlknimp  24687  wlkiswwlksur  24719  clwwlkf  24794  clwwlkextfrlem1  25076  grpoidinvlem3  25208  elspansn5  26492  5oalem6  26577  mdi  27214  dmdi  27221  dmdsl3  27234  atom1d  27272  cvexchlem  27287  atcvatlem  27304  chirredlem3  27311  mdsymlem5  27326  f1o3d  27471  dfon2lem6  29220  frmin  29322  soseq  29334  nodenselem5  29445  nodense  29449  broutsideof2  29772  outsideoftr  29779  outsideofeq  29780  nndivsub  29922  bddiblnc  30085  ftc1anc  30098  elicc3  30135  nn0prpwlem  30140  cntotbnd  30292  heiborlem6  30312  pridlc3  30470  funcrngcsetcALT  32807  bnj570  33963  leat2  35019  cvrexchlem  35143  cvratlem  35145  3dim2  35192  ps-2  35202  lncvrelatN  35505  osumcllem11N  35690

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