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

Theorem exp32 589
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 424 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
32exp3a 426 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  exp44  597  exp45  598  expr  599  anassrs  630  an13s  779  3impb  1149  ax11eq  2270  ax11el  2271  wereu  4578  reusv2lem2  4725  onint  4775  peano5  4868  funfvima3  5975  isomin  6057  isoini  6058  ovg  6212  tfrlem11  6649  tz7.48lem  6698  abianfplem  6715  oalimcl  6803  oaass  6804  resixpfo  7100  fundmen  7180  php3  7293  ssfi  7329  fodomfi  7385  marypha1lem  7438  card2inf  7523  ixpiunwdom  7559  cantnflt  7627  cnfcom  7657  dfac3  8002  dfac5lem5  8008  dfac5  8009  cfcoflem  8152  fin1a2s  8294  zorn2lem4  8379  zorn2lem7  8382  fpwwe2lem12  8516  wunfi  8596  grur1a  8694  addcanpi  8776  mulcanpi  8777  distrlem1pr  8902  ltaddpr  8911  ltexprlem1  8913  ltexprlem6  8918  ltexprlem7  8919  prodgt0  9855  mulgt1  9869  uzwo  10539  uzwoOLD  10540  xmulasslem  10864  xlemul1a  10867  faclbnd  11581  infpnlem1  13278  clatglble  14552  isacs4lem  14594  dmdprdsplit2lem  15603  pgpfac1  15638  pgpfac  15642  lssssr  16029  islmhm2  16114  lspdisj  16197  cygznlem2a  16848  neindisj  17181  cnpnei  17328  t0dist  17389  ordthauslem  17447  uncmp  17466  fiuncmp  17467  iunconlem  17490  fbasrn  17916  rnelfmlem  17984  rnelfm  17985  fmfnfmlem2  17987  fmfnfmlem4  17989  fclscf  18057  alexsubALTlem3  18080  alexsubALTlem4  18081  alexsubALT  18082  reconn  18859  fsumcn  18900  ovolfiniun  19397  dyadmax  19490  dyadmbllem  19491  dvmptfsum  19859  dvlip2  19879  dvivthlem1  19892  dvcnvrelem1  19901  ply1divex  20059  fta1g  20090  plydivex  20214  fta1  20225  mulcxp  20576  lgsquad2lem2  21143  pntlem3  21303  eupath2  21702  grpoidinvlem3  21794  grpoidinv  21796  shorth  22797  pjhthmo  22804  pjpjpre  22921  elspansn5  23076  lnopmi  23503  adjlnop  23589  leopmul2i  23638  stlesi  23744  ssmd2  23815  dmdsl3  23818  mdexchi  23838  cvexchlem  23871  atcv1  23883  atcvatlem  23888  atabsi  23904  mdsymlem2  23907  mdsymlem3  23908  mdsymlem5  23910  sumdmdii  23918  sumdmdlem  23921  sumdmdlem2  23922  dya2iocnrect  24631  pconcon  24918  iccllyscon  24937  trpredmintr  25509  poseq  25528  nodenselem8  25643  nocvxmin  25646  brbtwn  25838  brcgr  25839  brbtwn2  25844  axeuclid  25902  cgrextend  25942  btwnexch2  25957  colineardim1  25995  lineext  26010  btwnconn1lem13  26033  btwnconn1lem14  26034  seglecgr12im  26044  outsideofeq  26064  outsideofeu  26065  nndivsub  26207  ee7.2aOLD  26211  nn0prpwlem  26325  neibastop2lem  26389  tailfb  26406  filbcmb  26442  prdsbnd2  26504  heibor  26530  rngoisocnv  26597  mzpcompact2lem  26808  pellfundex  26949  acongsym  27041  pwssplit4  27168  pwslnm  27173  lindfmm  27274  stoweidlem17  27742  swrdccatin12lem3a  28208  swrdccat3  28215  bnj571  29277  pmodlem2  30644  lhpexle3lem  30808  lhpex2leN  30810  cdleme22b  31138  cdleme32d  31241  cdleme32f  31243  trlord  31366  cdlemg1cex  31385  cdlemj2  31619  cdlemk38  31712  cdlemk19x  31740  dihord2pre  32023
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 178  df-an 361
  Copyright terms: Public domain W3C validator