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

Theorem imp32 426
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
21imp3a 424 . 2
32imp 422 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362
This theorem is referenced by:  imp42  581  impr  606  anasss  632  an13s  786  3expb  1173  reuss2  3607  reupick  3611  po2nr  4625  tz7.7  4716  ordtr2  4734  fvmptt  5759  fliftfund  5974  isomin  5996  f1ocnv2d  6281  onint  6376  tz7.48lem  6855  oalimcl  6960  oaass  6961  omass  6980  omabs  7047  finsschain  7577  infxpenlem  8127  axcc3  8554  zorn2lem7  8618  addclpi  9007  addnidpi  9016  genpnnp  9120  genpnmax  9122  mulclprlem  9134  dedekindle  9480  prodgt0  10120  ltsubrp  10967  ltaddrp  10968  swrdccatin1  12315  swrdccat3  12324  infpnlem1  13911  iscatd  14551  imasmnd2  15398  imasgrp2  15607  imasrng  16535  0ntr  18379  clsndisj  18383  innei  18433  islpi  18457  tgcnp  18561  haust1  18660  alexsublem  19320  alexsubb  19322  isxmetd  19601  axcontlem4  22892  grpoidinvlem3  23372  elspansn5  24656  5oalem6  24741  mdi  25378  dmdi  25385  dmdsl3  25398  atom1d  25436  cvexchlem  25451  atcvatlem  25468  chirredlem3  25475  mdsymlem5  25490  f1o3d  25628  dfon2lem6  27303  frmin  27405  soseq  27417  nodenselem5  27528  nodense  27532  broutsideof2  27855  outsideoftr  27862  outsideofeq  27863  nndivsub  28006  bddiblnc  28133  ftc1anc  28146  elicc3  28183  nn0prpwlem  28188  cntotbnd  28366  heiborlem6  28386  pridlc3  28544  wwlknimp  29995  wlkiswwlksur  30025  clwwlkf  30130  clwwlkextfrlem1  30343  bnj570  31476  leat2  32376  cvrexchlem  32500  cvratlem  32502  3dim2  32549  ps-2  32559  lncvrelatN  32862  osumcllem11N  33047
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 179  df-an 364
  Copyright terms: Public domain W3C validator