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  2132  ax11el  2133  wereu  4389  tz7.7  4418  reusv2lem2  4536  onint  4586  peano5  4679  funfvima3  5755  isomin  5834  isoini  5835  isofrlem  5837  ovg  5986  tfrlem11  6404  tz7.48lem  6453  abianfplem  6470  oalimcl  6558  oaass  6559  resixpfo  6854  fundmen  6934  php3  7047  ssfi  7083  fodomfi  7135  marypha1lem  7186  card2inf  7269  ixpiunwdom  7305  cantnflt  7373  cnfcom  7403  cardaleph  7716  dfac3  7748  dfac5lem5  7754  dfac5  7755  cfcoflem  7898  coftr  7899  fin1a2s  8040  zorn2lem4  8126  zorn2lem7  8129  fpwwe2lem12  8263  wunfi  8343  grur1a  8441  grur1  8442  inaprc  8458  addcanpi  8523  mulcanpi  8524  distrlem1pr  8649  prlem934  8657  ltaddpr  8658  ltexprlem1  8660  ltexprlem6  8665  ltexprlem7  8666  reclem3pr  8673  00id  8987  mul02lem1  8988  addid2  8995  receu  9413  prodgt0  9601  mulgt1  9615  uzwo  10281  uzwoOLD  10282  xmulasslem  10605  xlemul1a  10608  faclbnd  11303  caucvgb  12152  dvdsval2  12534  infpnlem1  12957  clatglble  14229  isacs3lem  14269  isacs4lem  14271  dmdprdsplit2lem  15280  pgpfac1  15315  pgpfac  15319  lssssr  15710  islmhm2  15795  lspdisj  15878  drngnidl  15981  cygznlem2a  16521  tgcl  16707  neindisj  16854  restcls  16911  restntr  16912  cnpnei  16993  t0dist  17053  ordthauslem  17111  uncmp  17130  fiuncmp  17131  iunconlem  17153  2ndc1stc  17177  2ndcctbss  17181  fbasfip  17563  fbasrn  17579  elfm2  17643  elfm3  17645  rnelfmlem  17647  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  flffbas  17690  fclscf  17720  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  reconn  18333  fsumcn  18374  ovolfiniun  18860  dyadmax  18953  dyadmbllem  18954  dvmptfsum  19322  dvlip2  19342  dvivthlem1  19355  dvcnvrelem1  19364  ply1divex  19522  fta1g  19553  plydivex  19677  fta1  19688  aaliou3lem8  19725  aaliou3lem9  19730  mulcxp  20032  lgsquad2lem2  20598  pntlem3  20758  grpoidinvlem3  20873  grpoidinv  20875  shorth  21874  pjhthmo  21881  pjpjpre  21998  spansneleq  22149  elspansn5  22153  chscllem3  22218  lnopmi  22580  adjlnop  22666  leopmul2i  22715  stlesi  22821  ssmd2  22892  dmdsl3  22895  mdexchi  22915  cvexchlem  22948  atcv1  22960  atcvatlem  22965  atabsi  22981  mdsymlem2  22984  mdsymlem3  22985  mdsymlem5  22987  sumdmdii  22995  sumdmdlem  22998  sumdmdlem2  22999  xreceu  23105  pconcon  23762  iccllyscon  23781  eupath2  23904  trpredmintr  24234  poseq  24253  nodenselem5  24339  nodenselem8  24342  nocvxmin  24345  nobndlem6  24351  brbtwn  24527  brcgr  24528  brbtwn2  24533  colinearalg  24538  axeuclid  24591  cgrextend  24631  btwnexch2  24646  colineardim1  24684  lineext  24699  btwnconn1lem13  24722  btwnconn1lem14  24723  seglecgr12im  24733  outsideofeq  24753  outsideofeu  24754  outsidele  24755  nndivsub  24896  ee7.2aOLD  24900  11st22nd  25045  nn0prpwlem  26238  reftr  26289  neibastop2lem  26309  tailfb  26326  filbcmb  26432  prdsbnd2  26519  heiborlem8  26542  heibor  26545  rngoisocnv  26612  unichnidl  26656  mzpcompact2lem  26829  pellfundex  26971  acongsym  27063  acongrep  27067  jm2.27b  27099  pwssplit4  27191  pwslnm  27196  lindfmm  27297  bnj571  28938  cvlcvr1  29529  llnmlplnN  29728  cdlemb  29983  paddasslem10  30018  pmodlem2  30036  pexmidlem8N  30166  lhpexle3lem  30200  lhpex2leN  30202  trlcnv  30354  trlator0  30360  trlid0  30365  trlnidatb  30366  cdlemd4  30390  cdleme22b  30530  cdleme32d  30633  cdleme32f  30635  trlord  30758  cdlemg1cex  30777  cdlemg5  30794  trlco  30916  cdlemj2  31011  cdlemj3  31012  tendo0mul  31015  tendo0mulr  31016  tendoconid  31018  cdlemk38  31104  cdlemk19x  31132  erngdv  31182  erngdv-rN  31190  dihord2pre  31415  dihmeetlem1N  31480  dihatlat  31524  hgmaprnlem5N  32093
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