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

Theorem 3exp 1152
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 1133 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ph  /\  ps  /\  ch ) ) ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2syl8 67 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  3expa  1153  3expb  1154  3expia  1155  3expib  1156  3com23  1159  3an1rs  1165  3exp1  1169  3expd  1170  exp5o  1172  syl3an2  1218  syl3an3  1219  3ecase  1288  3impexpbicomi  1377  rexlimdv3a  2824  rabssdv  3415  reupick2  3619  disjss3  4203  wefrc  4568  tz7.7  4599  unizlim  4689  ssorduni  4757  suceloni  4784  tfisi  4829  sotriOLD  5257  f1oiso2  6063  poxp  6449  riotasv2dOLD  6586  riotasv3dOLD  6590  smo11  6617  odi  6813  omass  6814  nndi  6857  nnmass  6858  undifixp  7089  findcard  7338  ac6sfi  7342  domunfican  7370  fisup2g  7460  indcardi  7911  acndom  7921  ackbij1lem16  8104  infpssrlem4  8175  fin23lem11  8186  isfin2-2  8188  fin23lem34  8215  fin1a2lem10  8278  hsmexlem2  8296  axcc3  8307  domtriomlem  8311  axdc3lem2  8320  axdc3lem4  8322  axcclem  8326  ttukeyg  8386  axdclem2  8389  axacndlem4  8474  axacndlem5  8475  axacnd  8476  tskr1om2  8632  tskwe2  8637  tskord  8644  tskcard  8645  tskuni  8647  tskwun  8648  gruiin  8674  grudomon  8681  gruina  8682  mulcanpi  8766  adderpq  8822  mulerpq  8823  divgt0  9867  divge0  9868  uzind  10350  uzind2  10351  iccsplit  11018  sqlecan  11475  modexp  11502  facavg  11580  pceu  13208  mreexexd  13861  luble  14426  glble  14431  joinle  14438  meetle  14445  clatl  14531  isglbd  14532  mulgass2  15698  islss4  16026  lspsneu  16183  lspfixed  16188  lspexch  16189  lsmcv  16201  lspsolvlem  16202  xrsdsreclblem  16732  isphld  16873  fiinopn  16962  neips  17165  tpnei  17173  neindisj2  17175  opnneiid  17178  hausnei2  17405  cmpsublem  17450  cmpsub  17451  cmpcld  17453  bwth  17461  filufint  17940  cfinufil  17948  rnelfm  17973  alexsubALTlem1  18066  alexsubALTlem4  18069  alexsubALT  18070  tsmsxp  18172  neibl  18519  tgqioo  18819  ovolunlem2  19382  iunmbl2  19439  itg1le  19593  vieta1  20217  aannenlem2  20234  aalioulem3  20239  aalioulem4  20240  aaliou2  20245  wilthlem3  20841  bcmono  21049  usgrafisinds  21415  cusgrasize2inds  21474  1pthoncl  21580  wlkdvspth  21596  nvnencycllem  21618  gxid  21849  gxdi  21872  clmgm  21897  grpomndo  21922  zerdivemp1  22010  chintcli  22821  spansnss  23061  elspansn4  23063  chscllem4  23130  hoadddir  23295  adjmul  23583  kbass6  23612  stadd3i  23739  spansncv2  23784  sumdmdii  23906  dedekindle  25176  prodfn0  25211  prodfrec  25212  ntrivcvgfvn0  25216  fprodabs  25286  fprodefsum  25287  iprodefisumlem  25306  predpo  25439  poseq  25508  axcontlem7  25857  btwndiff  25909  bpolycl  26046  bpolydif  26049  elicc3  26257  finminlem  26258  comppfsc  26324  sdclem2  26383  zerdivemp1x  26508  mzpexpmpt  26739  pellexlem5  26833  pellex  26835  pell14qrexpclnn0  26866  pellfundex  26886  monotuz  26941  monotoddzzfi  26942  expmordi  26947  rmxypos  26949  jm2.17a  26962  jm2.17b  26963  rmygeid  26966  jm2.19lem3  26999  jm2.15nn0  27011  jm2.16nn0  27012  aomclem2  27067  aomclem6  27071  dfac11  27075  mapfien2  27173  hbtlem5  27247  cnsrexpcl  27285  pmtrfrn  27315  psgnunilem4  27335  refsumcn  27615  fmul01  27624  fmuldfeq  27627  fmul01lt1  27630  stoweidlem3  27666  stoweidlem31  27694  stoweidlem59  27722  stirlinglem13  27749  2shwrd2lem3  28144  n4cyclfrgra  28266  vdgfrgragt2  28276  ad4ant123  28398  ad4ant124  28399  ad4ant134  28400  ad4ant234  28403  ad5ant245  28411  ad5ant234  28412  ad5ant235  28413  ad5ant123  28414  ad5ant124  28415  ad5ant125  28416  ad5ant134  28417  ad5ant135  28418  ad5ant145  28419  ee333  28444  eel2221  28658  eel12131  28675  eel32131  28678  eel2122old  28682  e333  28699  ordelordALTVD  28833  bnj1417  29264  lsmsat  29645  lsmcv2  29666  lcvat  29667  lsatcveq0  29669  lcvexchlem4  29674  lcvexchlem5  29675  islshpcv  29690  l1cvpat  29691  lshpkrlem6  29752  omlfh3N  29896  cvlsupr4  29982  cvlsupr5  29983  cvlsupr6  29984  2llnneN  30045  hlrelat3  30048  cvrval3  30049  cvrval4N  30050  cvrexchlem  30055  2atlt  30075  cvrat4  30079  atbtwnexOLDN  30083  atbtwnex  30084  athgt  30092  3dim1  30103  3dim2  30104  3dim3  30105  1cvratex  30109  llnle  30154  atcvrlln2  30155  atcvrlln  30156  2llnmat  30160  lplnle  30176  lplnnle2at  30177  lplnnlelln  30179  llncvrlpln2  30193  2llnjN  30203  lvoli2  30217  lvolnlelln  30220  lvolnlelpln  30221  4atlem10  30242  4atlem11  30245  4atlem12  30248  lplncvrlvol2  30251  2lplnj  30256  lneq2at  30414  lnatexN  30415  lnjatN  30416  lncvrat  30418  2lnat  30420  cdlemb  30430  paddasslem14  30469  llnexchb2  30505  dalawlem10  30516  dalawlem13  30519  dalawlem14  30520  dalaw  30522  pclclN  30527  pclfinN  30536  osumcllem11N  30602  lhp2lt  30637  lhpexle3lem  30647  4atexlem7  30711  ldilcnv  30751  ldilco  30752  ltrncnv  30782  trlval2  30799  cdleme24  30988  cdleme26ee  30996  cdleme28  31009  cdleme32le  31083  cdleme50trn2  31187  cdleme50ltrn  31193  cdleme  31196  cdlemf1  31197  cdlemf  31199  cdlemg1cex  31224  cdlemg2ce  31228  cdlemg18b  31315  ltrnco  31355  tendocan  31460  cdlemk28-3  31544  cdlemk11t  31582  dia2dimlem6  31706  dia2dimlem12  31712  dihlsscpre  31871  dihord4  31895  dihord5b  31896  dihmeetlem3N  31942  dihmeetlem20N  31963  dvh4dimlem  32080  lclkrlem2y  32168  mapdpglem24  32341  mapdpglem32  32342  mapdpg  32343  baerlem3lem2  32347  baerlem5alem2  32348  baerlem5blem2  32349  mapdh9a  32427  mapdh9aOLDN  32428  hdmap14lem6  32513  hdmapglem7  32569
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  df-3an 938
  Copyright terms: Public domain W3C validator