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  1374  rexlimdv3a  2775  rabssdv  3366  reupick2  3570  disjss3  4152  wefrc  4517  tz7.7  4548  unizlim  4638  ssorduni  4706  suceloni  4733  tfisi  4778  sotriOLD  5206  f1oiso2  6011  poxp  6394  riotasv2dOLD  6531  riotasv3dOLD  6535  smo11  6562  odi  6758  omass  6759  nndi  6802  nnmass  6803  undifixp  7034  findcard  7283  ac6sfi  7287  domunfican  7315  fisup2g  7404  indcardi  7855  acndom  7865  ackbij1lem16  8048  infpssrlem4  8119  fin23lem11  8130  isfin2-2  8132  fin23lem34  8159  fin1a2lem10  8222  hsmexlem2  8240  axcc3  8251  domtriomlem  8255  axdc3lem2  8264  axdc3lem4  8266  axcclem  8270  ttukeyg  8330  axdclem2  8333  axacndlem4  8418  axacndlem5  8419  axacnd  8420  tskr1om2  8576  tskwe2  8581  tskord  8588  tskcard  8589  tskuni  8591  tskwun  8592  gruiin  8618  grudomon  8625  gruina  8626  mulcanpi  8710  adderpq  8766  mulerpq  8767  divgt0  9810  divge0  9811  uzind  10293  uzind2  10294  iccsplit  10961  sqlecan  11414  modexp  11441  facavg  11519  pceu  13147  mreexexd  13800  luble  14365  glble  14370  joinle  14377  meetle  14384  clatl  14470  isglbd  14471  mulgass2  15637  islss4  15965  lspsneu  16122  lspfixed  16127  lspexch  16128  lsmcv  16140  lspsolvlem  16141  xrsdsreclblem  16667  isphld  16808  fiinopn  16897  neips  17100  tpnei  17108  neindisj2  17110  opnneiid  17113  hausnei2  17339  cmpsublem  17384  cmpsub  17385  cmpcld  17387  filufint  17873  cfinufil  17881  rnelfm  17906  alexsubALTlem1  17999  alexsubALTlem4  18002  alexsubALT  18003  tsmsxp  18105  neibl  18421  tgqioo  18702  ovolunlem2  19261  iunmbl2  19318  itg1le  19472  vieta1  20096  aannenlem2  20113  aalioulem3  20118  aalioulem4  20119  aaliou2  20124  wilthlem3  20720  bcmono  20928  usgrafisinds  21293  cusgrasize2inds  21352  1pthoncl  21440  wlkdvspth  21456  nvnencycllem  21478  gxid  21709  gxdi  21732  clmgm  21757  grpomndo  21782  zerdivemp1  21870  chintcli  22681  spansnss  22921  elspansn4  22923  chscllem4  22990  hoadddir  23155  adjmul  23443  kbass6  23472  stadd3i  23599  spansncv2  23644  sumdmdii  23766  dedekindle  24967  prodfn0  25001  prodfrec  25002  ntrivcvgfvn0  25006  fprodabs  25076  fprodefsum  25077  predpo  25208  poseq  25277  axcontlem7  25623  btwndiff  25675  bpolycl  25812  bpolydif  25815  elicc3  26011  finminlem  26012  comppfsc  26078  sdclem2  26137  zerdivemp1x  26262  mzpexpmpt  26493  pellexlem5  26587  pellex  26589  pell14qrexpclnn0  26620  pellfundex  26640  monotuz  26695  monotoddzzfi  26696  expmordi  26701  rmxypos  26703  jm2.17a  26716  jm2.17b  26717  rmygeid  26720  jm2.19lem3  26753  jm2.15nn0  26765  jm2.16nn0  26766  aomclem2  26821  aomclem6  26825  dfac11  26829  mapfien2  26927  hbtlem5  27001  cnsrexpcl  27039  pmtrfrn  27069  psgnunilem4  27089  refsumcn  27369  fmul01  27378  fmuldfeq  27381  fmul01lt1  27384  stoweidlem3  27420  stoweidlem31  27448  stoweidlem59  27476  stirlinglem13  27503  n4cyclfrgra  27771  vdgfrgragt2  27781  ad4ant123  27886  ad4ant124  27887  ad4ant134  27888  ad4ant234  27891  ad5ant245  27899  ad5ant234  27900  ad5ant235  27901  ad5ant123  27902  ad5ant124  27903  ad5ant125  27904  ad5ant134  27905  ad5ant135  27906  ad5ant145  27907  ee333  27932  eel2221  28145  eel12131  28162  eel32131  28165  eel2122old  28169  e333  28186  ordelordALTVD  28320  bnj1417  28748  lsmsat  29123  lsmcv2  29144  lcvat  29145  lsatcveq0  29147  lcvexchlem4  29152  lcvexchlem5  29153  islshpcv  29168  l1cvpat  29169  lshpkrlem6  29230  omlfh3N  29374  cvlsupr4  29460  cvlsupr5  29461  cvlsupr6  29462  2llnneN  29523  hlrelat3  29526  cvrval3  29527  cvrval4N  29528  cvrexchlem  29533  2atlt  29553  cvrat4  29557  atbtwnexOLDN  29561  atbtwnex  29562  athgt  29570  3dim1  29581  3dim2  29582  3dim3  29583  1cvratex  29587  llnle  29632  atcvrlln2  29633  atcvrlln  29634  2llnmat  29638  lplnle  29654  lplnnle2at  29655  lplnnlelln  29657  llncvrlpln2  29671  2llnjN  29681  lvoli2  29695  lvolnlelln  29698  lvolnlelpln  29699  4atlem10  29720  4atlem11  29723  4atlem12  29726  lplncvrlvol2  29729  2lplnj  29734  lneq2at  29892  lnatexN  29893  lnjatN  29894  lncvrat  29896  2lnat  29898  cdlemb  29908  paddasslem14  29947  llnexchb2  29983  dalawlem10  29994  dalawlem13  29997  dalawlem14  29998  dalaw  30000  pclclN  30005  pclfinN  30014  osumcllem11N  30080  lhp2lt  30115  lhpexle3lem  30125  4atexlem7  30189  ldilcnv  30229  ldilco  30230  ltrncnv  30260  trlval2  30277  cdleme24  30466  cdleme26ee  30474  cdleme28  30487  cdleme32le  30561  cdleme50trn2  30665  cdleme50ltrn  30671  cdleme  30674  cdlemf1  30675  cdlemf  30677  cdlemg1cex  30702  cdlemg2ce  30706  cdlemg18b  30793  ltrnco  30833  tendocan  30938  cdlemk28-3  31022  cdlemk11t  31060  dia2dimlem6  31184  dia2dimlem12  31190  dihlsscpre  31349  dihord4  31373  dihord5b  31374  dihmeetlem3N  31420  dihmeetlem20N  31441  dvh4dimlem  31558  lclkrlem2y  31646  mapdpglem24  31819  mapdpglem32  31820  mapdpg  31821  baerlem3lem2  31825  baerlem5alem2  31826  baerlem5blem2  31827  mapdh9a  31905  mapdh9aOLDN  31906  hdmap14lem6  31991  hdmapglem7  32047
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