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  2198  ax11el  2199  wereu  4471  tz7.7  4500  reusv2lem2  4618  onint  4668  peano5  4761  funfvima3  5841  isomin  5921  isoini  5922  isofrlem  5924  ovg  6073  tfrlem11  6491  tz7.48lem  6540  abianfplem  6557  oalimcl  6645  oaass  6646  resixpfo  6942  fundmen  7022  php3  7135  ssfi  7171  fodomfi  7225  marypha1lem  7276  card2inf  7359  ixpiunwdom  7395  cantnflt  7463  cnfcom  7493  cardaleph  7806  dfac3  7838  dfac5lem5  7844  dfac5  7845  cfcoflem  7988  coftr  7989  fin1a2s  8130  zorn2lem4  8216  zorn2lem7  8219  fpwwe2lem12  8353  wunfi  8433  grur1a  8531  grur1  8532  inaprc  8548  addcanpi  8613  mulcanpi  8614  distrlem1pr  8739  prlem934  8747  ltaddpr  8748  ltexprlem1  8750  ltexprlem6  8755  ltexprlem7  8756  reclem3pr  8763  00id  9077  mul02lem1  9078  addid2  9085  receu  9503  prodgt0  9691  mulgt1  9705  uzwo  10373  uzwoOLD  10374  xmulasslem  10697  xlemul1a  10700  faclbnd  11396  caucvgb  12249  dvdsval2  12631  infpnlem1  13054  clatglble  14328  isacs3lem  14368  isacs4lem  14370  dmdprdsplit2lem  15379  pgpfac1  15414  pgpfac  15418  lssssr  15809  islmhm2  15894  lspdisj  15977  drngnidl  16080  cygznlem2a  16627  tgcl  16813  neindisj  16960  restcls  17017  restntr  17018  cnpnei  17099  t0dist  17159  ordthauslem  17217  uncmp  17236  fiuncmp  17237  iunconlem  17259  2ndc1stc  17283  2ndcctbss  17287  fbasfip  17665  fbasrn  17681  elfm2  17745  elfm3  17747  rnelfmlem  17749  rnelfm  17750  fmfnfmlem2  17752  fmfnfmlem4  17754  flffbas  17792  fclscf  17822  alexsubALTlem3  17845  alexsubALTlem4  17846  alexsubALT  17847  reconn  18436  fsumcn  18477  ovolfiniun  18964  dyadmax  19057  dyadmbllem  19058  dvmptfsum  19426  dvlip2  19446  dvivthlem1  19459  dvcnvrelem1  19468  ply1divex  19626  fta1g  19657  plydivex  19781  fta1  19792  aaliou3lem8  19829  aaliou3lem9  19834  mulcxp  20143  lgsquad2lem2  20710  pntlem3  20870  grpoidinvlem3  20985  grpoidinv  20987  shorth  21988  pjhthmo  21995  pjpjpre  22112  spansneleq  22263  elspansn5  22267  chscllem3  22332  lnopmi  22694  adjlnop  22780  leopmul2i  22829  stlesi  22935  ssmd2  23006  dmdsl3  23009  mdexchi  23029  cvexchlem  23062  atcv1  23074  atcvatlem  23079  atabsi  23095  mdsymlem2  23098  mdsymlem3  23099  mdsymlem5  23101  sumdmdii  23109  sumdmdlem  23112  sumdmdlem2  23113  xreceu  23372  dya2iocnrect  23895  pconcon  24166  iccllyscon  24185  eupath2  24308  trpredmintr  24792  poseq  24811  nodenselem5  24897  nodenselem8  24900  nocvxmin  24903  nobndlem6  24909  brbtwn  25086  brcgr  25087  brbtwn2  25092  colinearalg  25097  axeuclid  25150  cgrextend  25190  btwnexch2  25205  colineardim1  25243  lineext  25258  btwnconn1lem13  25281  btwnconn1lem14  25282  seglecgr12im  25292  outsideofeq  25312  outsideofeu  25313  outsidele  25314  nndivsub  25455  ee7.2aOLD  25459  nn0prpwlem  25562  reftr  25613  neibastop2lem  25633  tailfb  25650  filbcmb  25756  prdsbnd2  25842  heiborlem8  25865  heibor  25868  rngoisocnv  25935  unichnidl  25979  mzpcompact2lem  26152  pellfundex  26294  acongsym  26386  acongrep  26390  jm2.27b  26422  pwssplit4  26514  pwslnm  26519  lindfmm  26620  bnj571  28700  cvlcvr1  29598  llnmlplnN  29797  cdlemb  30052  paddasslem10  30087  pmodlem2  30105  pexmidlem8N  30235  lhpexle3lem  30269  lhpex2leN  30271  trlcnv  30423  trlator0  30429  trlid0  30434  trlnidatb  30435  cdlemd4  30459  cdleme22b  30599  cdleme32d  30702  cdleme32f  30704  trlord  30827  cdlemg1cex  30846  cdlemg5  30863  trlco  30985  cdlemj2  31080  cdlemj3  31081  tendo0mul  31084  tendo0mulr  31085  tendoconid  31087  cdlemk38  31173  cdlemk19x  31201  erngdv  31251  erngdv-rN  31259  dihord2pre  31484  dihmeetlem1N  31549  dihatlat  31593  hgmaprnlem5N  32162
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