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

Theorem 3exp 1150
Description: Exportation inference. (Contributed by NM, 30-May-1994.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3exp  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )

Proof of Theorem 3exp
StepHypRef Expression
1 pm3.2an3 1131 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ph  /\  ps  /\  ch ) ) ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2syl8 65 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  3expa  1151  3expb  1152  3expia  1153  3expib  1154  3com23  1157  3an1rs  1163  3exp1  1167  3expd  1168  exp5o  1170  syl3an2  1216  syl3an3  1217  3ecase  1286  3impexpbicomi  1358  rexlimdv3a  2669  rabssdv  3253  reupick2  3454  disjss3  4022  wefrc  4387  tz7.7  4418  unizlim  4509  ssorduni  4577  suceloni  4604  tfisi  4649  sotriOLD  5075  f1oiso2  5849  poxp  6227  riotasv2dOLD  6350  riotasv3dOLD  6354  smo11  6381  odi  6577  omass  6578  nndi  6621  nnmass  6622  undifixp  6852  findcard  7097  ac6sfi  7101  domunfican  7129  fisup2g  7217  indcardi  7668  acndom  7678  ackbij1lem16  7861  infpssrlem4  7932  fin23lem11  7943  isfin2-2  7945  fin23lem34  7972  fin1a2lem10  8035  hsmexlem2  8053  axcc3  8064  domtriomlem  8068  axdc3lem2  8077  axdc3lem4  8079  axcclem  8083  ttukeyg  8144  axdclem2  8147  axacndlem4  8232  axacndlem5  8233  axacnd  8234  tskr1om2  8390  tskwe2  8395  tskord  8402  tskcard  8403  tskuni  8405  tskwun  8406  gruiin  8432  grudomon  8439  gruina  8440  mulcanpi  8524  adderpq  8580  mulerpq  8581  divgt0  9624  divge0  9625  uzind  10103  uzind2  10104  iccsplit  10768  sqlecan  11209  modexp  11236  facavg  11314  pceu  12899  mreexexd  13550  luble  14115  glble  14120  joinle  14127  meetle  14134  clatl  14220  isglbd  14221  mulgass2  15387  islss4  15719  lspsneu  15876  lspfixed  15881  lspexch  15882  lsmcv  15894  lspsolvlem  15895  xrsdsreclblem  16417  isphld  16558  fiinopn  16647  neips  16850  tpnei  16858  neindisj2  16860  opnneiid  16863  hausnei2  17081  cmpsublem  17126  cmpsub  17127  cmpcld  17129  filufint  17615  cfinufil  17623  rnelfm  17648  alexsubALTlem1  17741  alexsubALTlem4  17744  alexsubALT  17745  tsmsxp  17837  neibl  18047  tgqioo  18306  ovolunlem2  18857  iunmbl2  18914  itg1le  19068  vieta1  19692  aannenlem2  19709  aalioulem3  19714  aalioulem4  19715  aaliou2  19720  wilthlem3  20308  bcmono  20516  gxid  20940  gxdi  20963  clmgm  20988  grpomndo  21013  chintcli  21910  spansnss  22150  elspansn4  22152  chscllem4  22219  hoadddir  22384  adjmul  22672  kbass6  22701  stadd3i  22828  spansncv2  22873  sumdmdii  22995  dedekindle  24083  predpo  24184  poseq  24253  axcontlem7  24598  btwndiff  24650  bpolycl  24787  bpolydif  24790  and4as  24939  prl  25167  prl2  25169  oriso  25214  geme2  25275  latdir  25295  reacomsmgrp2  25344  resgcom  25351  grpodivone  25373  grpodivfo  25374  grpodlcan  25376  trran2  25393  trinv  25395  ltrooo  25404  zerdivemp1  25436  mvecrtol2  25477  muldisc  25481  glmrngo  25482  svli2  25484  svs2  25487  truni3  25507  fisub  25554  cmptdst  25568  prdnei  25573  limptlimpr2lem1  25574  limptlimpr2lem2  25575  islimrs3  25581  islimrs4  25582  bwt2  25592  iintlem1  25610  lvsovso  25626  lvsovso2  25627  addcomv  25655  addcanri  25666  negveud  25668  negveudr  25669  issubcv  25670  subaddv  25671  subclrvd  25674  distsava  25689  icccon4  25702  hdrmp  25706  cmphmia  25798  cmphmib  25799  iri  25800  cmpassoh  25801  homgrf  25802  cmpmon  25815  icmpmon  25816  iepiclem  25823  tartarmap  25888  eltintpar  25899  inttaror  25900  fnctartar  25907  fnctartar2  25908  prismorcsetlemb  25913  cmpmor  25975  setiscat  25979  pgapspf2  26053  isconcl5a  26101  isconcl5ab  26102  isibg1a6  26125  bsstr  26128  nbssntr  26129  segline  26141  pxysxy  26142  lppotos  26144  bosser  26167  pdiveql  26168  elicc3  26228  finminlem  26231  comppfsc  26307  sdclem2  26452  zerdivemp1x  26586  mzpexpmpt  26823  pellexlem5  26918  pellex  26920  pell14qrexpclnn0  26951  pellfundex  26971  monotuz  27026  monotoddzzfi  27027  expmordi  27032  rmxypos  27034  jm2.17a  27047  jm2.17b  27048  rmygeid  27051  jm2.19lem3  27084  jm2.15nn0  27096  jm2.16nn0  27097  aomclem2  27152  aomclem6  27156  dfac11  27160  mapfien2  27258  hbtlem5  27332  cnsrexpcl  27370  pmtrfrn  27400  psgnunilem4  27420  refsumcn  27701  fmul01  27710  fmuldfeq  27713  fmul01lt1  27716  stoweidlem3  27752  stoweidlem31  27780  stoweidlem57  27806  stoweidlem59  27808  stirlinglem13  27835  ee333  28268  eel2221  28476  eel2122old  28497  e333  28508  ordelordALTVD  28643  bnj1417  29071  a12study4  29117  lsmsat  29198  lsmcv2  29219  lcvat  29220  lsatcveq0  29222  lcvexchlem4  29227  lcvexchlem5  29228  islshpcv  29243  l1cvpat  29244  lshpkrlem6  29305  omlfh3N  29449  cvlsupr4  29535  cvlsupr5  29536  cvlsupr6  29537  2llnneN  29598  hlrelat3  29601  cvrval3  29602  cvrval4N  29603  cvrexchlem  29608  2atlt  29628  cvrat4  29632  atbtwnexOLDN  29636  atbtwnex  29637  athgt  29645  3dim1  29656  3dim2  29657  3dim3  29658  1cvratex  29662  llnle  29707  atcvrlln2  29708  atcvrlln  29709  2llnmat  29713  lplnle  29729  lplnnle2at  29730  lplnnlelln  29732  llncvrlpln2  29746  2llnjN  29756  lvoli2  29770  lvolnlelln  29773  lvolnlelpln  29774  4atlem10  29795  4atlem11  29798  4atlem12  29801  lplncvrlvol2  29804  2lplnj  29809  lneq2at  29967  lnatexN  29968  lnjatN  29969  lncvrat  29971  2lnat  29973  cdlemb  29983  paddasslem14  30022  llnexchb2  30058  dalawlem10  30069  dalawlem13  30072  dalawlem14  30073  dalaw  30075  pclclN  30080  pclfinN  30089  osumcllem11N  30155  lhp2lt  30190  lhpexle3lem  30200  4atexlem7  30264  ldilcnv  30304  ldilco  30305  ltrncnv  30335  trlval2  30352  cdleme24  30541  cdleme26ee  30549  cdleme28  30562  cdleme32le  30636  cdleme50trn2  30740  cdleme50ltrn  30746  cdleme  30749  cdlemf1  30750  cdlemf  30752  cdlemg1cex  30777  cdlemg2ce  30781  cdlemg18b  30868  ltrnco  30908  tendocan  31013  cdlemk28-3  31097  cdlemk11t  31135  dia2dimlem6  31259  dia2dimlem12  31265  dihlsscpre  31424  dihord4  31448  dihord5b  31449  dihmeetlem3N  31495  dihmeetlem20N  31516  dvh4dimlem  31633  lclkrlem2y  31721  mapdpglem24  31894  mapdpglem32  31895  mapdpg  31896  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902  mapdh9a  31980  mapdh9aOLDN  31981  hdmap14lem6  32066  hdmapglem7  32122
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  df-3an 936
  Copyright terms: Public domain W3C validator