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

Theorem exp32 588
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp32.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
exp32  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )

Proof of Theorem exp32
StepHypRef Expression
1 exp32.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21ex 423 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
32exp3a 425 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  exp44  596  exp45  597  expr  598  anassrs  629  an13s  778  3impb  1147  ax11eq  2165  ax11el  2166  wereu  4426  tz7.7  4455  reusv2lem2  4573  onint  4623  peano5  4716  funfvima3  5796  isomin  5876  isoini  5877  isofrlem  5879  ovg  6028  tfrlem11  6446  tz7.48lem  6495  abianfplem  6512  oalimcl  6600  oaass  6601  resixpfo  6897  fundmen  6977  php3  7090  ssfi  7126  fodomfi  7180  marypha1lem  7231  card2inf  7314  ixpiunwdom  7350  cantnflt  7418  cnfcom  7448  cardaleph  7761  dfac3  7793  dfac5lem5  7799  dfac5  7800  cfcoflem  7943  coftr  7944  fin1a2s  8085  zorn2lem4  8171  zorn2lem7  8174  fpwwe2lem12  8308  wunfi  8388  grur1a  8486  grur1  8487  inaprc  8503  addcanpi  8568  mulcanpi  8569  distrlem1pr  8694  prlem934  8702  ltaddpr  8703  ltexprlem1  8705  ltexprlem6  8710  ltexprlem7  8711  reclem3pr  8718  00id  9032  mul02lem1  9033  addid2  9040  receu  9458  prodgt0  9646  mulgt1  9660  uzwo  10328  uzwoOLD  10329  xmulasslem  10652  xlemul1a  10655  faclbnd  11350  caucvgb  12199  dvdsval2  12581  infpnlem1  13004  clatglble  14278  isacs3lem  14318  isacs4lem  14320  dmdprdsplit2lem  15329  pgpfac1  15364  pgpfac  15368  lssssr  15759  islmhm2  15844  lspdisj  15927  drngnidl  16030  cygznlem2a  16577  tgcl  16763  neindisj  16910  restcls  16967  restntr  16968  cnpnei  17049  t0dist  17109  ordthauslem  17167  uncmp  17186  fiuncmp  17187  iunconlem  17209  2ndc1stc  17233  2ndcctbss  17237  fbasfip  17615  fbasrn  17631  elfm2  17695  elfm3  17697  rnelfmlem  17699  rnelfm  17700  fmfnfmlem2  17702  fmfnfmlem4  17704  flffbas  17742  fclscf  17772  alexsubALTlem3  17795  alexsubALTlem4  17796  alexsubALT  17797  reconn  18385  fsumcn  18426  ovolfiniun  18913  dyadmax  19006  dyadmbllem  19007  dvmptfsum  19375  dvlip2  19395  dvivthlem1  19408  dvcnvrelem1  19417  ply1divex  19575  fta1g  19606  plydivex  19730  fta1  19741  aaliou3lem8  19778  aaliou3lem9  19783  mulcxp  20085  lgsquad2lem2  20651  pntlem3  20811  grpoidinvlem3  20926  grpoidinv  20928  shorth  21929  pjhthmo  21936  pjpjpre  22053  spansneleq  22204  elspansn5  22208  chscllem3  22273  lnopmi  22635  adjlnop  22721  leopmul2i  22770  stlesi  22876  ssmd2  22947  dmdsl3  22950  mdexchi  22970  cvexchlem  23003  atcv1  23015  atcvatlem  23020  atabsi  23036  mdsymlem2  23039  mdsymlem3  23040  mdsymlem5  23042  sumdmdii  23050  sumdmdlem  23053  sumdmdlem2  23054  xreceu  23320  dya2iocnrect  23805  pconcon  24046  iccllyscon  24065  eupath2  24188  trpredmintr  24619  poseq  24638  nodenselem5  24724  nodenselem8  24727  nocvxmin  24730  nobndlem6  24736  brbtwn  24913  brcgr  24914  brbtwn2  24919  colinearalg  24924  axeuclid  24977  cgrextend  25017  btwnexch2  25032  colineardim1  25070  lineext  25085  btwnconn1lem13  25108  btwnconn1lem14  25109  seglecgr12im  25119  outsideofeq  25139  outsideofeu  25140  outsidele  25141  nndivsub  25282  ee7.2aOLD  25286  nn0prpwlem  25387  reftr  25438  neibastop2lem  25458  tailfb  25475  filbcmb  25581  prdsbnd2  25667  heiborlem8  25690  heibor  25693  rngoisocnv  25760  unichnidl  25804  mzpcompact2lem  25977  pellfundex  26119  acongsym  26211  acongrep  26215  jm2.27b  26247  pwssplit4  26339  pwslnm  26344  lindfmm  26445  bnj571  28449  cvlcvr1  29347  llnmlplnN  29546  cdlemb  29801  paddasslem10  29836  pmodlem2  29854  pexmidlem8N  29984  lhpexle3lem  30018  lhpex2leN  30020  trlcnv  30172  trlator0  30178  trlid0  30183  trlnidatb  30184  cdlemd4  30208  cdleme22b  30348  cdleme32d  30451  cdleme32f  30453  trlord  30576  cdlemg1cex  30595  cdlemg5  30612  trlco  30734  cdlemj2  30829  cdlemj3  30830  tendo0mul  30833  tendo0mulr  30834  tendoconid  30836  cdlemk38  30922  cdlemk19x  30950  erngdv  31000  erngdv-rN  31008  dihord2pre  31233  dihmeetlem1N  31298  dihatlat  31342  hgmaprnlem5N  31911
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator