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

Theorem 3exp 1204
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 1184 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ph  /\  ps  /\  ch ) ) ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2syl8 72 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984
This theorem is referenced by:  3expa  1205  3expb  1206  3expia  1207  3expib  1208  3com23  1211  3an1rs  1217  3exp1  1221  3expd  1222  exp5o  1224  ad4ant123  1232  ad4ant124  1233  ad4ant134  1234  ad4ant234  1237  ad5ant245  1245  ad5ant234  1246  ad5ant235  1247  ad5ant123  1248  ad5ant124  1249  ad5ant125  1250  ad5ant134  1251  ad5ant135  1252  ad5ant145  1253  syl3an2  1298  syl3an3  1299  3ecase  1369  rexlimdv3a  2858  rabssdv  3484  reupick2  3702  disjss3  4365  wefrc  4790  predpo  5360  tz7.7  5411  unizlim  5501  fveqdmss  5976  f1oiso2  6202  ssorduni  6570  suceloni  6598  tfisi  6643  poxp  6863  smo11  7038  tfrlem5  7053  odi  7235  omass  7236  nndi  7279  nnmass  7280  undifixp  7513  findcard  7763  ac6sfi  7768  domunfican  7797  mapfien2  7875  fisup2g  7937  fiinf2g  7969  indcardi  8423  acndom  8433  ackbij1lem16  8616  infpssrlem4  8687  fin23lem11  8698  isfin2-2  8700  fin23lem34  8727  fin1a2lem10  8790  hsmexlem2  8808  axcc3  8819  domtriomlem  8823  axdc3lem2  8832  axdc3lem4  8834  axcclem  8838  ttukeyg  8898  axdclem2  8901  axacndlem4  8986  axacndlem5  8987  axacnd  8988  tskr1om2  9144  tskwe2  9149  tskord  9156  tskcard  9157  tskuni  9159  tskwun  9160  gruiin  9186  grudomon  9193  gruina  9194  mulcanpi  9276  adderpq  9332  mulerpq  9333  dedekindle  9749  divgt0  10424  divge0  10425  uzind  10978  uzind2  10979  iccsplit  11716  ssnn0fi  12147  sqlecan  12331  modexp  12357  facavg  12436  2cshwcshw  12870  relexpcnv  13042  relexpreld  13047  relexpaddnn  13058  relexpaddg  13060  prodfn0  13893  prodfrec  13894  ntrivcvgfvn0  13898  fprodabs  13971  fprodle  13993  bpolycl  14048  bpolydif  14051  fprodefsum  14092  ncoprmlnprm  14620  pceu  14739  mreexexd  15497  initoeu1  15849  termoeu1  15856  isglbd  16306  pmtrfrn  17042  psgnunilem4  17081  mulgass2  17772  islss4  18128  lspsneu  18289  lspfixed  18294  lspexch  18295  lsmcv  18307  lspsolvlem  18308  xrsdsreclblem  18957  isphld  19163  mdetralt  19575  mdetunilem9  19587  fiinopn  19873  neips  20071  tpnei  20079  neindisj2  20081  opnneiid  20084  hausnei2  20311  cmpsublem  20356  cmpsub  20357  cmpcld  20359  comppfsc  20489  filufint  20877  cfinufil  20885  rnelfm  20910  alexsubALTlem1  21004  alexsubALTlem4  21007  alexsubALT  21008  tsmsxp  21111  neibl  21458  tgqioo  21760  ovolunlem2  22393  iunmbl2  22452  itg1le  22613  vieta1  23207  aannenlem2  23227  aalioulem3  23232  aalioulem4  23233  aaliou2  23238  wilthlem3  23937  bcmono  24147  axcontlem7  24942  usgrafisinds  25083  cusgrasize2inds  25147  1pthoncl  25264  wlkdvspth  25280  nvnencycllem  25313  wwlknred  25393  wwlknextbi  25395  clwlkfclwwlk  25514  cusgraiffrusgra  25610  n4cyclfrgra  25688  vdgfrgragt2  25697  usgn0fidegnn0  25699  frgraregord013  25788  gxid  25943  gxdi  25966  clmgmOLD  25991  grpomndo  26016  zerdivemp1  26104  chintcli  26926  spansnss  27166  elspansn4  27168  chscllem4  27235  hoadddir  27399  adjmul  27687  kbass6  27716  stadd3i  27843  spansncv2  27888  sumdmdii  28010  nexple  28783  bnj1417  29802  mclsind  30160  iprodefisumlem  30327  poseq  30442  btwndiff  30743  elicc3  30922  finminlem  30923  sdclem2  31978  zerdivemp1x  32101  lsmsat  32486  lsmcv2  32507  lcvat  32508  lsatcveq0  32510  lcvexchlem4  32515  lcvexchlem5  32516  islshpcv  32531  l1cvpat  32532  lshpkrlem6  32593  omlfh3N  32737  cvlsupr4  32823  cvlsupr5  32824  cvlsupr6  32825  2llnneN  32886  hlrelat3  32889  cvrval3  32890  cvrval4N  32891  cvrexchlem  32896  2atlt  32916  cvrat4  32920  atbtwnexOLDN  32924  atbtwnex  32925  athgt  32933  3dim1  32944  3dim2  32945  3dim3  32946  1cvratex  32950  llnle  32995  atcvrlln2  32996  atcvrlln  32997  2llnmat  33001  lplnle  33017  lplnnle2at  33018  lplnnlelln  33020  llncvrlpln2  33034  2llnjN  33044  lvoli2  33058  lvolnlelln  33061  lvolnlelpln  33062  4atlem10  33083  4atlem11  33086  4atlem12  33089  lplncvrlvol2  33092  2lplnj  33097  lneq2at  33255  lnatexN  33256  lnjatN  33257  lncvrat  33259  2lnat  33261  cdlemb  33271  paddasslem14  33310  llnexchb2  33346  dalawlem10  33357  dalawlem13  33360  dalawlem14  33361  dalaw  33363  pclclN  33368  pclfinN  33377  osumcllem11N  33443  lhp2lt  33478  lhpexle3lem  33488  4atexlem7  33552  ldilcnv  33592  ldilco  33593  ltrncnv  33623  trlval2  33641  cdleme24  33831  cdleme26ee  33839  cdleme28  33852  cdleme32le  33926  cdleme50trn2  34030  cdleme50ltrn  34036  cdleme  34039  cdlemf1  34040  cdlemf  34042  cdlemg1cex  34067  cdlemg2ce  34071  cdlemg18b  34158  ltrnco  34198  tendocan  34303  cdlemk28-3  34387  cdlemk11t  34425  dia2dimlem6  34549  dia2dimlem12  34555  dihlsscpre  34714  dihord4  34738  dihord5b  34739  dihmeetlem3N  34785  dihmeetlem20N  34806  dvh4dimlem  34923  lclkrlem2y  35011  mapdpglem24  35184  mapdpglem32  35185  mapdpg  35186  baerlem3lem2  35190  baerlem5alem2  35191  baerlem5blem2  35192  mapdh9a  35270  mapdh9aOLDN  35271  hdmap14lem6  35356  hdmapglem7  35412  mzpexpmpt  35499  pellexlem5  35590  pellex  35592  pell14qrexpclnn0  35625  pellfundex  35647  monotuz  35702  monotoddzzfi  35703  expmordi  35708  rmxypos  35710  jm2.17a  35723  jm2.17b  35724  rmygeid  35727  jm2.19lem3  35759  jm2.15nn0  35771  jm2.16nn0  35772  aomclem2  35826  aomclem6  35830  dfac11  35833  hbtlem5  35900  cnsrexpcl  35944  relexpxpnnidm  36208  relexpiidm  36209  relexpss1d  36210  iunrelexpmin1  36213  relexpmulnn  36214  iunrelexpmin2  36217  relexp01min  36218  relexp0a  36221  relexpxpmin  36222  relexpaddss  36223  trclimalb2  36231  3impexpbicomi  36748  ee333  36776  eel2221  36996  eel12131  37013  eel32131  37016  eel2122old  37019  e333  37036  ordelordALTVD  37180  refsumcn  37267  uzwo4  37308  suprnmpt  37342  wessf1ornlem  37363  disjf1o  37370  fompt  37371  disjinfi  37372  ssnnf1octb  37374  fperiodmullem  37418  upbdrech  37420  ssfiunibd  37424  supxrgere  37453  iuneqfzuzlem  37454  supxrgelem  37457  supxrge  37458  suplesup  37459  infrpge  37471  iccshift  37511  iooshift  37515  fmul01  37541  fmuldfeq  37544  fmul01lt1  37547  mullimc  37579  islptre  37582  mullimcf  37586  limcperiod  37591  islpcn  37602  limsupre  37604  limsupreOLD  37605  limcleqr  37608  neglimc  37611  addlimc  37612  0ellimcdiv  37613  limclner  37615  coskpi2  37624  cosknegpi  37627  cncfshift  37634  cncfperiod  37639  icccncfext  37648  dvnmptdivc  37696  dvnmptconst  37699  dvnmul  37701  dvmptfprodlem  37702  dvmptfprod  37703  dvnprodlem1  37704  dvnprodlem2  37705  iblspltprt  37733  itgspltprt  37739  itgperiod  37741  stoweidlem3  37746  stoweidlem31  37775  stoweidlem59  37803  stirlinglem13  37831  fourierdlem41  37894  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem48  37901  fourierdlem51  37904  fourierdlem53  37906  fourierdlem70  37923  fourierdlem71  37924  fourierdlem73  37926  fourierdlem80  37933  fourierdlem81  37934  fourierdlem89  37942  fourierdlem91  37944  fourierdlem93  37946  fourierdlem97  37950  elaa2  37982  sge0tsms  38073  sge0f1o  38075  sge0fsum  38080  sge0supre  38082  sge0sup  38084  sge0rnbnd  38086  sge0gerp  38088  sge0pnffigt  38089  sge0lefi  38091  sge0ltfirp  38093  sge0resrn  38097  sge0resplit  38099  sge0split  38102  sge0iunmptlemfi  38106  sge0iunmptlemre  38108  sge0iunmpt  38111  sge0rpcpnf  38114  sge0isum  38120  sge0xp  38122  sge0xaddlem2  38127  sge0uzfsumgt  38137  nnfoctbdjlem  38144  nnfoctbdj  38145  iundjiun  38149  meadjiunlem  38154  carageniuncllem1  38193  carageniuncllem2  38194  caratheodorylem1  38198  caratheodorylem2  38199  isomenndlem  38202  ovnsupge0  38226  ovnlerp  38231  ovncvrrp  38233  ovnsubaddlem1  38239  hoidmvval0  38256  hoidmv1lelem3  38262  hoidmv1le  38263  hoidmvlelem1  38264  hoidmvlelem2  38265  hoidmvlelem3  38266  ovnhoilem2  38271  iccpartiltu  38549  fundmge2nop  38833  uhgrauhgrbi  38937  ausgrumgri  39019  ausgrusgri  39020  usgrausgrb  39021  usgredg2vtx  39057  usgredg2vtxeuALT  39059  usgredgedga  39064  nbuhgr2vtx1edgb  39166  cusgrsize2inds  39252  uhgrauhgbi  39287  rngccatidALTV  39592  ringccatidALTV  39655  nzerooringczr  39675  lcosslsp  39834  fllog2  39982  dignn0flhalf  40032
  Copyright terms: Public domain W3C validator