MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3exp Structured version   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  2832  rabssdv  3423  reupick2  3627  disjss3  4211  wefrc  4576  tz7.7  4607  unizlim  4698  ssorduni  4766  suceloni  4793  tfisi  4838  sotriOLD  5266  f1oiso2  6072  poxp  6458  riotasv2dOLD  6595  riotasv3dOLD  6599  smo11  6626  odi  6822  omass  6823  nndi  6866  nnmass  6867  undifixp  7098  findcard  7347  ac6sfi  7351  domunfican  7379  fisup2g  7471  indcardi  7922  acndom  7932  ackbij1lem16  8115  infpssrlem4  8186  fin23lem11  8197  isfin2-2  8199  fin23lem34  8226  fin1a2lem10  8289  hsmexlem2  8307  axcc3  8318  domtriomlem  8322  axdc3lem2  8331  axdc3lem4  8333  axcclem  8337  ttukeyg  8397  axdclem2  8400  axacndlem4  8485  axacndlem5  8486  axacnd  8487  tskr1om2  8643  tskwe2  8648  tskord  8655  tskcard  8656  tskuni  8658  tskwun  8659  gruiin  8685  grudomon  8692  gruina  8693  mulcanpi  8777  adderpq  8833  mulerpq  8834  divgt0  9878  divge0  9879  uzind  10361  uzind2  10362  iccsplit  11029  sqlecan  11487  modexp  11514  facavg  11592  pceu  13220  mreexexd  13873  luble  14438  glble  14443  joinle  14450  meetle  14457  clatl  14543  isglbd  14544  mulgass2  15710  islss4  16038  lspsneu  16195  lspfixed  16200  lspexch  16201  lsmcv  16213  lspsolvlem  16214  xrsdsreclblem  16744  isphld  16885  fiinopn  16974  neips  17177  tpnei  17185  neindisj2  17187  opnneiid  17190  hausnei2  17417  cmpsublem  17462  cmpsub  17463  cmpcld  17465  bwth  17473  filufint  17952  cfinufil  17960  rnelfm  17985  alexsubALTlem1  18078  alexsubALTlem4  18081  alexsubALT  18082  tsmsxp  18184  neibl  18531  tgqioo  18831  ovolunlem2  19394  iunmbl2  19451  itg1le  19605  vieta1  20229  aannenlem2  20246  aalioulem3  20251  aalioulem4  20252  aaliou2  20257  wilthlem3  20853  bcmono  21061  usgrafisinds  21427  cusgrasize2inds  21486  1pthoncl  21592  wlkdvspth  21608  nvnencycllem  21630  gxid  21861  gxdi  21884  clmgm  21909  grpomndo  21934  zerdivemp1  22022  chintcli  22833  spansnss  23073  elspansn4  23075  chscllem4  23142  hoadddir  23307  adjmul  23595  kbass6  23624  stadd3i  23751  spansncv2  23796  sumdmdii  23918  dedekindle  25188  prodfn0  25222  prodfrec  25223  ntrivcvgfvn0  25227  fprodabs  25297  fprodefsum  25298  iprodefisumlem  25317  predpo  25459  poseq  25528  axcontlem7  25909  btwndiff  25961  bpolycl  26098  bpolydif  26101  elicc3  26320  finminlem  26321  comppfsc  26387  sdclem2  26446  zerdivemp1x  26571  mzpexpmpt  26802  pellexlem5  26896  pellex  26898  pell14qrexpclnn0  26929  pellfundex  26949  monotuz  27004  monotoddzzfi  27005  expmordi  27010  rmxypos  27012  jm2.17a  27025  jm2.17b  27026  rmygeid  27029  jm2.19lem3  27062  jm2.15nn0  27074  jm2.16nn0  27075  aomclem2  27130  aomclem6  27134  dfac11  27137  mapfien2  27235  hbtlem5  27309  cnsrexpcl  27347  pmtrfrn  27377  psgnunilem4  27397  refsumcn  27677  fmul01  27686  fmuldfeq  27689  fmul01lt1  27692  stoweidlem3  27728  stoweidlem31  27756  stoweidlem59  27784  stirlinglem13  27811  2cshw2lem3  28254  n4cyclfrgra  28408  vdgfrgragt2  28418  ad4ant123  28540  ad4ant124  28541  ad4ant134  28542  ad4ant234  28545  ad5ant245  28553  ad5ant234  28554  ad5ant235  28555  ad5ant123  28556  ad5ant124  28557  ad5ant125  28558  ad5ant134  28559  ad5ant135  28560  ad5ant145  28561  ee333  28589  eel2221  28804  eel12131  28821  eel32131  28824  eel2122old  28828  e333  28845  ordelordALTVD  28979  bnj1417  29410  lsmsat  29806  lsmcv2  29827  lcvat  29828  lsatcveq0  29830  lcvexchlem4  29835  lcvexchlem5  29836  islshpcv  29851  l1cvpat  29852  lshpkrlem6  29913  omlfh3N  30057  cvlsupr4  30143  cvlsupr5  30144  cvlsupr6  30145  2llnneN  30206  hlrelat3  30209  cvrval3  30210  cvrval4N  30211  cvrexchlem  30216  2atlt  30236  cvrat4  30240  atbtwnexOLDN  30244  atbtwnex  30245  athgt  30253  3dim1  30264  3dim2  30265  3dim3  30266  1cvratex  30270  llnle  30315  atcvrlln2  30316  atcvrlln  30317  2llnmat  30321  lplnle  30337  lplnnle2at  30338  lplnnlelln  30340  llncvrlpln2  30354  2llnjN  30364  lvoli2  30378  lvolnlelln  30381  lvolnlelpln  30382  4atlem10  30403  4atlem11  30406  4atlem12  30409  lplncvrlvol2  30412  2lplnj  30417  lneq2at  30575  lnatexN  30576  lnjatN  30577  lncvrat  30579  2lnat  30581  cdlemb  30591  paddasslem14  30630  llnexchb2  30666  dalawlem10  30677  dalawlem13  30680  dalawlem14  30681  dalaw  30683  pclclN  30688  pclfinN  30697  osumcllem11N  30763  lhp2lt  30798  lhpexle3lem  30808  4atexlem7  30872  ldilcnv  30912  ldilco  30913  ltrncnv  30943  trlval2  30960  cdleme24  31149  cdleme26ee  31157  cdleme28  31170  cdleme32le  31244  cdleme50trn2  31348  cdleme50ltrn  31354  cdleme  31357  cdlemf1  31358  cdlemf  31360  cdlemg1cex  31385  cdlemg2ce  31389  cdlemg18b  31476  ltrnco  31516  tendocan  31621  cdlemk28-3  31705  cdlemk11t  31743  dia2dimlem6  31867  dia2dimlem12  31873  dihlsscpre  32032  dihord4  32056  dihord5b  32057  dihmeetlem3N  32103  dihmeetlem20N  32124  dvh4dimlem  32241  lclkrlem2y  32329  mapdpglem24  32502  mapdpglem32  32503  mapdpg  32504  baerlem3lem2  32508  baerlem5alem2  32509  baerlem5blem2  32510  mapdh9a  32588  mapdh9aOLDN  32589  hdmap14lem6  32674  hdmapglem7  32730
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