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

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
StepHypRef Expression
1 imp3.1 . . 3
21impd 431 . 2
32imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  imp42  594  impr  619  anasss  647  an13s  801  3expb  1189  reuss2  3744  reupick  3748  po2nr  4771  tz7.7  4862  ordtr2  4880  fvmptt  5912  fliftfund  6137  isomin  6159  f1ocnv2d  6444  onint  6539  tz7.48lem  7030  oalimcl  7133  oaass  7134  omass  7153  omabs  7220  finsschain  7753  infxpenlem  8317  axcc3  8744  zorn2lem7  8808  addclpi  9198  addnidpi  9207  genpnnp  9311  genpnmax  9313  mulclprlem  9325  dedekindle  9671  prodgt0  10311  ltsubrp  11161  ltaddrp  11162  swrdccatin1  12532  swrdccat3  12541  infpnlem1  14129  iscatd  14770  imasmnd2  15617  imasgrp2  15829  imasrng  16887  mplcoe5lem  17724  dmatmul  18587  scmatmulcl  18606  scmatsgrp1  18610  cpmatacl  18789  cpmatmcllem  18791  0ntr  19074  clsndisj  19078  innei  19128  islpi  19152  tgcnp  19256  haust1  19355  alexsublem  20015  alexsubb  20017  isxmetd  20300  axcontlem4  23682  grpoidinvlem3  24162  elspansn5  25446  5oalem6  25531  mdi  26168  dmdi  26175  dmdsl3  26188  atom1d  26226  cvexchlem  26241  atcvatlem  26258  chirredlem3  26265  mdsymlem5  26280  f1o3d  26416  dfon2lem6  28057  frmin  28159  soseq  28171  nodenselem5  28282  nodense  28286  broutsideof2  28609  outsideoftr  28616  outsideofeq  28617  nndivsub  28759  bddiblnc  28922  ftc1anc  28935  elicc3  28972  nn0prpwlem  28977  cntotbnd  29155  heiborlem6  29175  pridlc3  29333  wwlknimp  31198  wlkiswwlksur  31228  clwwlkf  31333  clwwlkextfrlem1  31546  bnj570  32741  leat2  33790  cvrexchlem  33914  cvratlem  33916  3dim2  33963  ps-2  33973  lncvrelatN  34276  osumcllem11N  34461
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