Theorem 3exp 1194

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

Step	Hyp	Ref	Expression
1		pm3.2an3 1174	. 2 |- ( ph -> ( ps -> ( ch -> ( ph /\ ps /\ ch ) ) ) )
2		3exp.1	. 2 |- ( ( ph /\ ps /\ ch ) -> th )
3	1, 2	syl8 70	1 |- ( ph -> ( ps -> ( ch -> th ) ) )

Syntax hints:   -> wi 4   /\ w3a 972

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 185  df-an 371  df-3an 974

This theorem is referenced by:  3expa  1195  3expb  1196  3expia  1197  3expib  1198  3com23  1201  3an1rs  1207  3exp1  1211  3expd  1212  exp5o  1214  syl3an2  1261  syl3an3  1262  3ecase  1332  rexlimdv3a  2935  rabssdv  3563  reupick2  3767  disjss3  4433  wefrc  4860  tz7.7  4891  unizlim  4981  sotriOLD  5386  fveqdmss  6008  f1oiso2  6230  ssorduni  6603  suceloni  6630  tfisi  6675  poxp  6894  smo11  7034  tfrlem5  7048  odi  7227  omass  7228  nndi  7271  nnmass  7272  undifixp  7504  findcard  7758  ac6sfi  7763  domunfican  7792  mapfien2  7867  fisup2g  7926  indcardi  8422  acndom  8432  ackbij1lem16  8615  infpssrlem4  8686  fin23lem11  8697  isfin2-2  8699  fin23lem34  8726  fin1a2lem10  8789  hsmexlem2  8807  axcc3  8818  domtriomlem  8822  axdc3lem2  8831  axdc3lem4  8833  axcclem  8837  ttukeyg  8897  axdclem2  8900  axacndlem4  8988  axacndlem5  8989  axacnd  8990  tskr1om2  9146  tskwe2  9151  tskord  9158  tskcard  9159  tskuni  9161  tskwun  9162  gruiin  9188  grudomon  9195  gruina  9196  mulcanpi  9278  adderpq  9334  mulerpq  9335  dedekindle  9745  divgt0  10413  divge0  10414  uzind  10957  uzind2  10958  iccsplit  11659  ssnn0fi  12070  sqlecan  12250  modexp  12277  facavg  12355  2cshwcshw  12769  pceu  14244  mreexexd  14919  isglbd  15618  pmtrfrn  16354  psgnunilem4  16393  mulgass2  17118  islss4  17479  lspsneu  17640  lspfixed  17645  lspexch  17646  lsmcv  17658  lspsolvlem  17659  xrsdsreclblem  18335  isphld  18559  mdetralt  18980  mdetunilem9  18992  fiinopn  19280  neips  19484  tpnei  19492  neindisj2  19494  opnneiid  19497  hausnei2  19724  cmpsublem  19769  cmpsub  19770  cmpcld  19772  bwthOLD  19781  comppfsc  19903  filufint  20291  cfinufil  20299  rnelfm  20324  alexsubALTlem1  20417  alexsubALTlem4  20420  alexsubALT  20421  tsmsxp  20527  neibl  20874  tgqioo  21175  ovolunlem2  21779  iunmbl2  21837  itg1le  21990  vieta1  22577  aannenlem2  22594  aalioulem3  22599  aalioulem4  22600  aaliou2  22605  wilthlem3  23213  bcmono  23421  axcontlem7  24142  usgrafisinds  24282  cusgrasize2inds  24346  1pthoncl  24463  wlkdvspth  24479  nvnencycllem  24512  wwlknred  24592  wwlknextbi  24594  clwlkfclwwlk  24713  cusgraiffrusgra  24809  n4cyclfrgra  24887  vdgfrgragt2  24896  usgn0fidegnn0  24898  frgraregord013  24987  gxid  25144  gxdi  25167  clmgmOLD  25192  grpomndo  25217  zerdivemp1  25305  chintcli  26118  spansnss  26358  elspansn4  26360  chscllem4  26427  hoadddir  26592  adjmul  26880  kbass6  26909  stadd3i  27036  spansncv2  27081  sumdmdii  27203  nexple  27875  mclsind  28800  prodfn0  29000  prodfrec  29001  ntrivcvgfvn0  29005  fprodabs  29075  fprodefsum  29076  iprodefisumlem  29095  predpo  29236  poseq  29305  btwndiff  29649  bpolycl  29786  bpolydif  29789  elicc3  30107  finminlem  30108  sdclem2  30207  zerdivemp1x  30330  mzpexpmpt  30649  pellexlem5  30741  pellex  30743  pell14qrexpclnn0  30774  pellfundex  30794  monotuz  30849  monotoddzzfi  30850  expmordi  30855  rmxypos  30857  jm2.17a  30870  jm2.17b  30871  rmygeid  30874  jm2.19lem3  30905  jm2.15nn0  30917  jm2.16nn0  30918  aomclem2  30973  aomclem6  30977  dfac11  30980  mapfien2OLD  31014  hbtlem5  31049  cnsrexpcl  31087  refsumcn  31356  suprnmpt  31401  fperiodmullem  31452  upbdrech  31454  ssfiunibd  31458  iccshift  31494  iooshift  31498  fmul01  31502  fmuldfeq  31505  fmul01lt1  31508  mullimc  31530  islptre  31533  mullimcf  31537  limcperiod  31542  islpcn  31553  limsupre  31555  limcleqr  31558  neglimc  31561  addlimc  31562  0ellimcdiv  31563  limclner  31565  coskpi2  31573  cosknegpi  31576  cncfshift  31583  cncfperiod  31588  icccncfext  31597  iblspltprt  31662  itgspltprt  31668  itgperiod  31670  stoweidlem3  31674  stoweidlem31  31702  stoweidlem59  31730  stirlinglem13  31757  fourierdlem41  31819  fourierdlem42  31820  fourierdlem48  31826  fourierdlem51  31829  fourierdlem53  31831  fourierdlem70  31848  fourierdlem71  31849  fourierdlem73  31851  fourierdlem80  31858  fourierdlem81  31859  fourierdlem89  31867  fourierdlem91  31869  fourierdlem93  31871  fourierdlem97  31875  uhgrauhgbi  32212  rngccatidOLD  32534  ringccatidOLD  32592  lcosslsp  32769  3impexpbicomi  32950  ad4ant123  32954  ad4ant124  32955  ad4ant134  32956  ad4ant234  32959  ad5ant245  32967  ad5ant234  32968  ad5ant235  32969  ad5ant123  32970  ad5ant124  32971  ad5ant125  32972  ad5ant134  32973  ad5ant135  32974  ad5ant145  32975  ee333  33004  eel2221  33217  eel12131  33234  eel32131  33237  eel2122old  33241  e333  33258  ordelordALTVD  33395  bnj1417  33825  lsmsat  34456  lsmcv2  34477  lcvat  34478  lsatcveq0  34480  lcvexchlem4  34485  lcvexchlem5  34486  islshpcv  34501  l1cvpat  34502  lshpkrlem6  34563  omlfh3N  34707  cvlsupr4  34793  cvlsupr5  34794  cvlsupr6  34795  2llnneN  34856  hlrelat3  34859  cvrval3  34860  cvrval4N  34861  cvrexchlem  34866  2atlt  34886  cvrat4  34890  atbtwnexOLDN  34894  atbtwnex  34895  athgt  34903  3dim1  34914  3dim2  34915  3dim3  34916  1cvratex  34920  llnle  34965  atcvrlln2  34966  atcvrlln  34967  2llnmat  34971  lplnle  34987  lplnnle2at  34988  lplnnlelln  34990  llncvrlpln2  35004  2llnjN  35014  lvoli2  35028  lvolnlelln  35031  lvolnlelpln  35032  4atlem10  35053  4atlem11  35056  4atlem12  35059  lplncvrlvol2  35062  2lplnj  35067  lneq2at  35225  lnatexN  35226  lnjatN  35227  lncvrat  35229  2lnat  35231  cdlemb  35241  paddasslem14  35280  llnexchb2  35316  dalawlem10  35327  dalawlem13  35330  dalawlem14  35331  dalaw  35333  pclclN  35338  pclfinN  35347  osumcllem11N  35413  lhp2lt  35448  lhpexle3lem  35458  4atexlem7  35522  ldilcnv  35562  ldilco  35563  ltrncnv  35593  trlval2  35611  cdleme24  35801  cdleme26ee  35809  cdleme28  35822  cdleme32le  35896  cdleme50trn2  36000  cdleme50ltrn  36006  cdleme  36009  cdlemf1  36010  cdlemf  36012  cdlemg1cex  36037  cdlemg2ce  36041  cdlemg18b  36128  ltrnco  36168  tendocan  36273  cdlemk28-3  36357  cdlemk11t  36395  dia2dimlem6  36519  dia2dimlem12  36525  dihlsscpre  36684  dihord4  36708  dihord5b  36709  dihmeetlem3N  36755  dihmeetlem20N  36776  dvh4dimlem  36893  lclkrlem2y  36981  mapdpglem24  37154  mapdpglem32  37155  mapdpg  37156  baerlem3lem2  37160  baerlem5alem2  37161  baerlem5blem2  37162  mapdh9a  37240  mapdh9aOLDN  37241  hdmap14lem6  37326  hdmapglem7  37382