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  2682  rabssdv  3266  reupick2  3467  disjss3  4038  wefrc  4403  tz7.7  4434  unizlim  4525  ssorduni  4593  suceloni  4620  tfisi  4665  sotriOLD  5091  f1oiso2  5865  poxp  6243  riotasv2dOLD  6366  riotasv3dOLD  6370  smo11  6397  odi  6593  omass  6594  nndi  6637  nnmass  6638  undifixp  6868  findcard  7113  ac6sfi  7117  domunfican  7145  fisup2g  7233  indcardi  7684  acndom  7694  ackbij1lem16  7877  infpssrlem4  7948  fin23lem11  7959  isfin2-2  7961  fin23lem34  7988  fin1a2lem10  8051  hsmexlem2  8069  axcc3  8080  domtriomlem  8084  axdc3lem2  8093  axdc3lem4  8095  axcclem  8099  ttukeyg  8160  axdclem2  8163  axacndlem4  8248  axacndlem5  8249  axacnd  8250  tskr1om2  8406  tskwe2  8411  tskord  8418  tskcard  8419  tskuni  8421  tskwun  8422  gruiin  8448  grudomon  8455  gruina  8456  mulcanpi  8540  adderpq  8596  mulerpq  8597  divgt0  9640  divge0  9641  uzind  10119  uzind2  10120  iccsplit  10784  sqlecan  11225  modexp  11252  facavg  11330  pceu  12915  mreexexd  13566  luble  14131  glble  14136  joinle  14143  meetle  14150  clatl  14236  isglbd  14237  mulgass2  15403  islss4  15735  lspsneu  15892  lspfixed  15897  lspexch  15898  lsmcv  15910  lspsolvlem  15911  xrsdsreclblem  16433  isphld  16574  fiinopn  16663  neips  16866  tpnei  16874  neindisj2  16876  opnneiid  16879  hausnei2  17097  cmpsublem  17142  cmpsub  17143  cmpcld  17145  filufint  17631  cfinufil  17639  rnelfm  17664  alexsubALTlem1  17757  alexsubALTlem4  17760  alexsubALT  17761  tsmsxp  17853  neibl  18063  tgqioo  18322  ovolunlem2  18873  iunmbl2  18930  itg1le  19084  vieta1  19708  aannenlem2  19725  aalioulem3  19730  aalioulem4  19731  aaliou2  19736  wilthlem3  20324  bcmono  20532  gxid  20956  gxdi  20979  clmgm  21004  grpomndo  21029  chintcli  21926  spansnss  22166  elspansn4  22168  chscllem4  22235  hoadddir  22400  adjmul  22688  kbass6  22717  stadd3i  22844  spansncv2  22889  sumdmdii  23011  dedekindle  24098  faclim  24126  predpo  24255  poseq  24324  axcontlem7  24670  btwndiff  24722  bpolycl  24859  bpolydif  24862  and4as  25042  prl  25270  prl2  25272  oriso  25317  geme2  25378  latdir  25398  reacomsmgrp2  25447  resgcom  25454  grpodivone  25476  grpodivfo  25477  grpodlcan  25479  trran2  25496  trinv  25498  ltrooo  25507  zerdivemp1  25539  mvecrtol2  25580  muldisc  25584  glmrngo  25585  svli2  25587  svs2  25590  truni3  25610  fisub  25657  cmptdst  25671  prdnei  25676  limptlimpr2lem1  25677  limptlimpr2lem2  25678  islimrs3  25684  islimrs4  25685  bwt2  25695  iintlem1  25713  lvsovso  25729  lvsovso2  25730  addcomv  25758  addcanri  25769  negveud  25771  negveudr  25772  issubcv  25773  subaddv  25774  subclrvd  25777  distsava  25792  icccon4  25805  hdrmp  25809  cmphmia  25901  cmphmib  25902  iri  25903  cmpassoh  25904  homgrf  25905  cmpmon  25918  icmpmon  25919  iepiclem  25926  tartarmap  25991  eltintpar  26002  inttaror  26003  fnctartar  26010  fnctartar2  26011  prismorcsetlemb  26016  cmpmor  26078  setiscat  26082  pgapspf2  26156  isconcl5a  26204  isconcl5ab  26205  isibg1a6  26228  bsstr  26231  nbssntr  26232  segline  26244  pxysxy  26245  lppotos  26247  bosser  26270  pdiveql  26271  elicc3  26331  finminlem  26334  comppfsc  26410  sdclem2  26555  zerdivemp1x  26689  mzpexpmpt  26926  pellexlem5  27021  pellex  27023  pell14qrexpclnn0  27054  pellfundex  27074  monotuz  27129  monotoddzzfi  27130  expmordi  27135  rmxypos  27137  jm2.17a  27150  jm2.17b  27151  rmygeid  27154  jm2.19lem3  27187  jm2.15nn0  27199  jm2.16nn0  27200  aomclem2  27255  aomclem6  27259  dfac11  27263  mapfien2  27361  hbtlem5  27435  cnsrexpcl  27473  pmtrfrn  27503  psgnunilem4  27523  refsumcn  27804  fmul01  27813  fmuldfeq  27816  fmul01lt1  27819  stoweidlem3  27855  stoweidlem31  27883  stoweidlem57  27909  stoweidlem59  27911  stirlinglem13  27938  wlkdvspth  28366  nvnencycllem  28389  n4cyclfrgra  28440  ad4ant123  28521  ad4ant124  28522  ad4ant134  28523  ad4ant234  28526  ad5ant245  28534  ad5ant234  28535  ad5ant235  28536  ad5ant123  28537  ad5ant124  28538  ad5ant125  28539  ad5ant134  28540  ad5ant135  28541  ad5ant145  28542  ee333  28567  eel2221  28781  eel12131  28798  eel32131  28801  eel2122old  28805  e333  28822  ordelordALTVD  28959  bnj1417  29387  a12study4  29739  lsmsat  29820  lsmcv2  29841  lcvat  29842  lsatcveq0  29844  lcvexchlem4  29849  lcvexchlem5  29850  islshpcv  29865  l1cvpat  29866  lshpkrlem6  29927  omlfh3N  30071  cvlsupr4  30157  cvlsupr5  30158  cvlsupr6  30159  2llnneN  30220  hlrelat3  30223  cvrval3  30224  cvrval4N  30225  cvrexchlem  30230  2atlt  30250  cvrat4  30254  atbtwnexOLDN  30258  atbtwnex  30259  athgt  30267  3dim1  30278  3dim2  30279  3dim3  30280  1cvratex  30284  llnle  30329  atcvrlln2  30330  atcvrlln  30331  2llnmat  30335  lplnle  30351  lplnnle2at  30352  lplnnlelln  30354  llncvrlpln2  30368  2llnjN  30378  lvoli2  30392  lvolnlelln  30395  lvolnlelpln  30396  4atlem10  30417  4atlem11  30420  4atlem12  30423  lplncvrlvol2  30426  2lplnj  30431  lneq2at  30589  lnatexN  30590  lnjatN  30591  lncvrat  30593  2lnat  30595  cdlemb  30605  paddasslem14  30644  llnexchb2  30680  dalawlem10  30691  dalawlem13  30694  dalawlem14  30695  dalaw  30697  pclclN  30702  pclfinN  30711  osumcllem11N  30777  lhp2lt  30812  lhpexle3lem  30822  4atexlem7  30886  ldilcnv  30926  ldilco  30927  ltrncnv  30957  trlval2  30974  cdleme24  31163  cdleme26ee  31171  cdleme28  31184  cdleme32le  31258  cdleme50trn2  31362  cdleme50ltrn  31368  cdleme  31371  cdlemf1  31372  cdlemf  31374  cdlemg1cex  31399  cdlemg2ce  31403  cdlemg18b  31490  ltrnco  31530  tendocan  31635  cdlemk28-3  31719  cdlemk11t  31757  dia2dimlem6  31881  dia2dimlem12  31887  dihlsscpre  32046  dihord4  32070  dihord5b  32071  dihmeetlem3N  32117  dihmeetlem20N  32138  dvh4dimlem  32255  lclkrlem2y  32343  mapdpglem24  32516  mapdpglem32  32517  mapdpg  32518  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524  mapdh9a  32602  mapdh9aOLDN  32603  hdmap14lem6  32688  hdmapglem7  32744
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