Theorem 3exp 1264

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 1240	. 2 |- ( ph -> ( ps -> ( ch -> ( ph /\ ps /\ ch ) ) ) )
2		3exp.1	. 2 |- ( ( ph /\ ps /\ ch ) -> th )
3	1, 2	syl8 76	1 |- ( ph -> ( ps -> ( ch -> th ) ) )

Syntax hints:   -> wi 4   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3expa  1265  3expb  1266  3expia  1267  3expib  1268  3com23  1271  3imp3i2an  1278  3an1rs  1279  3exp1  1283  3expd  1284  exp5o  1286  ad4ant123  1294  ad4ant124  1295  ad4ant134  1296  ad4ant234  1299  ad5ant245  1307  ad5ant234  1308  ad5ant235  1309  ad5ant123  1310  ad5ant124  1311  ad5ant125  1312  ad5ant134  1313  ad5ant135  1314  ad5ant145  1315  syl3an2  1360  syl3an3  1361  syl2an23an  1387  3ecase  1437  rexlimdv3a  3033  rabssdv  3682  reupick2  3913  disjiund  4643  otiunsndisj  4980  wefrc  5108  predpo  5698  tz7.7  5749  unizlim  5844  fveqdmss  6354  f1oiso2  6602  ssorduni  6985  suceloni  7013  tfisi  7058  poxp  7289  smo11  7461  tfrlem5  7476  odi  7659  omass  7660  nndi  7703  nnmass  7704  undifixp  7944  findcard  8199  ac6sfi  8204  domunfican  8233  mapfien2  8314  fisup2g  8374  fiinf2g  8406  indcardi  8864  acndom  8874  ackbij1lem16  9057  infpssrlem4  9128  fin23lem11  9139  isfin2-2  9141  fin23lem34  9168  fin1a2lem10  9231  hsmexlem2  9249  axcc3  9260  domtriomlem  9264  axdc3lem2  9273  axdc3lem4  9275  axcclem  9279  ttukeyg  9339  axdclem2  9342  axacndlem4  9432  axacndlem5  9433  axacnd  9434  tskr1om2  9590  tskwe2  9595  tskord  9602  tskcard  9603  tskuni  9605  tskwun  9606  gruiin  9632  grudomon  9639  gruina  9640  mulcanpi  9722  adderpq  9778  mulerpq  9779  dedekindle  10201  divgt0  10891  divge0  10892  uzind  11469  uzind2  11470  iccsplit  12305  ssnn0fi  12784  sqlecan  12971  modexp  12999  facavg  13088  2cshwcshw  13571  relexpcnv  13775  relexpreld  13780  relexpaddnn  13791  relexpaddg  13793  prodfn0  14626  prodfrec  14627  ntrivcvgfvn0  14631  fprodabs  14704  fprodle  14727  bpolycl  14783  bpolydif  14786  fprodefsum  14825  dvdsaddre2b  15029  dvdsnprmd  15403  prmndvdsfaclt  15435  ncoprmlnprm  15436  pceu  15551  setsstruct2  15896  setsstruct  15898  mreexexd  16308  mreexexdOLD  16309  initoeu1  16661  termoeu1  16668  isglbd  17117  mulgaddcom  17564  pmtrfrn  17878  psgnunilem4  17917  mulgass2  18601  islss4  18962  lspsneu  19123  lspfixed  19128  lspexch  19129  lsmcv  19141  lspsolvlem  19142  xrsdsreclblem  19792  isphld  19999  mdetralt  20414  mdetunilem9  20426  fiinopn  20706  neips  20917  tpnei  20925  neindisj2  20927  opnneiid  20930  hausnei2  21157  cmpsublem  21202  cmpsub  21203  cmpcld  21205  comppfsc  21335  filufint  21724  cfinufil  21732  rnelfm  21757  alexsubALTlem1  21851  alexsubALTlem4  21854  alexsubALT  21855  tsmsxp  21958  neibl  22306  tngngp3  22460  tgqioo  22603  ovolunlem2  23266  iunmbl2  23325  itg1le  23480  vieta1  24067  aannenlem2  24084  aalioulem3  24089  aalioulem4  24090  aaliou2  24095  wilthlem3  24796  bcmono  25002  gausslemma2dlem1a  25090  axcontlem7  25850  edglnl  26038  numedglnl  26039  ausgrumgri  26062  ausgrusgri  26063  usgrausgrb  26064  usgredg2vtxeuALT  26114  ushgredgedg  26121  ushgredgedgloop  26123  nbuhgr2vtx1edgb  26248  cusgrsize2inds  26349  upgrewlkle2  26502  wlkl1loop  26534  redwlk  26569  pthdivtx  26625  pthdadjvtx  26626  upgr2pthnlp  26628  upgrspthswlk  26634  clwlkl1loop  26678  wwlksnred  26787  wwlksnextbi  26789  elwwlks2ons3  26848  umgrwwlks2on  26850  clwwlkinwwlk  26905  clwwnisshclwwsn  26930  clwlksfclwwlk  26962  1pthon2v  27013  uhgr3cyclex  27042  n4cyclfrgr  27155  frgrwopreg  27187  clwwlksnwwlksn  27209  numclwwlkffin0  27215  frgrreggt1  27251  frgrreg  27252  frgrregord013  27253  chintcli  28190  spansnss  28430  elspansn4  28432  chscllem4  28499  hoadddir  28663  adjmul  28951  kbass6  28980  spansncv2  29152  sumdmdii  29274  nexple  30071  bnj1417  31109  mclsind  31467  iprodefisumlem  31626  poseq  31750  btwndiff  32134  elicc3  32311  finminlem  32312  sdclem2  33538  clmgmOLD  33650  grpomndo  33674  zerdivemp1x  33746  lsmsat  34295  lsmcv2  34316  lcvat  34317  lsatcveq0  34319  lcvexchlem4  34324  lcvexchlem5  34325  islshpcv  34340  l1cvpat  34341  lshpkrlem6  34402  omlfh3N  34546  cvlsupr4  34632  cvlsupr5  34633  cvlsupr6  34634  2llnneN  34695  hlrelat3  34698  cvrval3  34699  cvrval4N  34700  cvrexchlem  34705  2atlt  34725  cvrat4  34729  atbtwnexOLDN  34733  atbtwnex  34734  athgt  34742  3dim1  34753  3dim2  34754  3dim3  34755  1cvratex  34759  llnle  34804  atcvrlln2  34805  atcvrlln  34806  2llnmat  34810  lplnle  34826  lplnnle2at  34827  lplnnlelln  34829  llncvrlpln2  34843  2llnjN  34853  lvoli2  34867  lvolnlelln  34870  lvolnlelpln  34871  4atlem10  34892  4atlem11  34895  4atlem12  34898  lplncvrlvol2  34901  2lplnj  34906  lneq2at  35064  lnatexN  35065  lnjatN  35066  lncvrat  35068  2lnat  35070  cdlemb  35080  paddasslem14  35119  llnexchb2  35155  dalawlem10  35166  dalawlem13  35169  dalawlem14  35170  dalaw  35172  pclclN  35177  pclfinN  35186  osumcllem11N  35252  lhp2lt  35287  lhpexle3lem  35297  4atexlem7  35361  ldilcnv  35401  ldilco  35402  ltrncnv  35432  trlval2  35450  cdleme24  35640  cdleme26ee  35648  cdleme28  35661  cdleme32le  35735  cdleme50trn2  35839  cdleme50ltrn  35845  cdleme  35848  cdlemf1  35849  cdlemf  35851  cdlemg1cex  35876  cdlemg2ce  35880  cdlemg18b  35967  ltrnco  36007  tendocan  36112  cdlemk28-3  36196  cdlemk11t  36234  dia2dimlem6  36358  dia2dimlem12  36364  dihlsscpre  36523  dihord4  36547  dihord5b  36548  dihmeetlem3N  36594  dihmeetlem20N  36615  dvh4dimlem  36732  lclkrlem2y  36820  mapdpglem24  36993  mapdpglem32  36994  mapdpg  36995  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  mapdh9a  37079  mapdh9aOLDN  37080  hdmap14lem6  37165  hdmapglem7  37221  mzpexpmpt  37308  pellexlem5  37397  pellex  37399  pell14qrexpclnn0  37430  pellfundex  37450  monotuz  37506  monotoddzzfi  37507  expmordi  37512  rmxypos  37514  jm2.17a  37527  jm2.17b  37528  rmygeid  37531  jm2.19lem3  37558  jm2.15nn0  37570  jm2.16nn0  37571  aomclem2  37625  aomclem6  37629  dfac11  37632  hbtlem5  37698  cnsrexpcl  37735  relexpxpnnidm  37995  relexpiidm  37996  relexpss1d  37997  iunrelexpmin1  38000  relexpmulnn  38001  iunrelexpmin2  38004  relexp01min  38005  relexp0a  38008  relexpxpmin  38009  relexpaddss  38010  trclimalb2  38018  3impexpbicomi  38686  ee333  38713  eel12131  38938  eel2122old  38943  e333  38960  ordelordALTVD  39103  refsumcn  39189  uzwo4  39221  ssinc  39264  ssdec  39265  iunincfi  39272  restuni3  39301  eliuniin2  39303  rabssd  39332  reximdd  39344  suprnmpt  39355  wessf1ornlem  39371  disjf1o  39378  fompt  39379  disjinfi  39380  ssnnf1octb  39382  mapsnd  39388  choicefi  39392  mapssbi  39405  unirnmapsn  39406  ssmapsn  39408  iunmapsn  39409  funimassd  39431  rnmptlb  39453  rnmptbddlem  39455  fvelimad  39458  infnsuprnmpt  39465  fperiodmullem  39517  upbdrech  39519  ssfiunibd  39523  supxrgere  39549  iuneqfzuzlem  39550  supxrgelem  39553  supxrge  39554  suplesup  39555  infrpge  39567  infleinf  39588  suplesup2  39592  supxrunb3  39623  infleinf2  39641  rexabslelem  39645  infrnmptle  39650  infxrunb3rnmpt  39655  iccshift  39744  iooshift  39748  fmul01  39812  fmuldfeq  39815  fmul01lt1  39818  mullimc  39848  islptre  39851  mullimcf  39855  limcperiod  39860  islpcn  39871  limsupre  39873  limcleqr  39876  neglimc  39879  addlimc  39880  0ellimcdiv  39881  limclner  39883  fnlimfvre  39906  limsuppnflem  39942  limsupmnfuzlem  39958  limsupre3lem  39964  limsupre3uzlem  39967  climuzlem  39975  limsupgtlem  40009  coskpi2  40077  cosknegpi  40080  cncfshift  40087  cncfperiod  40092  icccncfext  40100  dvnmptdivc  40153  dvnmptconst  40156  dvnmul  40158  dvmptfprodlem  40159  dvmptfprod  40160  dvnprodlem1  40161  dvnprodlem2  40162  iblspltprt  40189  itgspltprt  40195  itgperiod  40197  ismbl3  40203  stoweidlem3  40220  stoweidlem31  40248  stoweidlem59  40276  stirlinglem13  40303  fourierdlem41  40365  fourierdlem42  40366  fourierdlem48  40371  fourierdlem51  40374  fourierdlem53  40376  fourierdlem70  40393  fourierdlem71  40394  fourierdlem73  40396  fourierdlem80  40403  fourierdlem81  40404  fourierdlem89  40412  fourierdlem91  40414  fourierdlem93  40416  fourierdlem97  40420  elaa2  40451  qndenserrnopnlem  40517  salexct  40552  subsaliuncl  40576  subsalsal  40577  sge0tsms  40597  sge0f1o  40599  sge0fsum  40604  sge0supre  40606  sge0sup  40608  sge0rnbnd  40610  sge0gerp  40612  sge0pnffigt  40613  sge0lefi  40615  sge0ltfirp  40617  sge0resrn  40621  sge0resplit  40623  sge0split  40626  sge0iunmptlemfi  40630  sge0iunmptlemre  40632  sge0iunmpt  40635  sge0rpcpnf  40638  sge0isum  40644  sge0xp  40646  sge0xaddlem2  40651  sge0uzfsumgt  40661  sge0seq  40663  sge0reuz  40664  nnfoctbdjlem  40672  nnfoctbdj  40673  iundjiun  40677  meadjiunlem  40682  voliunsge0lem  40689  meaiuninclem  40697  meaiininc2  40702  carageniuncllem1  40735  carageniuncllem2  40736  caratheodorylem1  40740  caratheodorylem2  40741  isomenndlem  40744  ovnsupge0  40771  ovnlerp  40776  ovncvrrp  40778  ovnsubaddlem1  40784  hoidmvval0  40801  hoidmv1lelem3  40807  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  ovnhoilem2  40816  opnvonmbllem2  40847  ovolval5lem3  40868  ovnovollem3  40872  vonioo  40896  vonicc  40899  pimiooltgt  40921  sssmf  40947  smfaddlem1  40971  smflimlem6  40984  smfmullem4  41001  smfpimbor1lem1  41005  smfco  41009  smfpimcc  41014  smflimmpt  41016  smfinflem  41023  smflimsuplem7  41032  smflimsuplem8  41033  smflimsupmpt  41035  smfliminfmpt  41038  iccpartiltu  41358  goldbachth  41459  fmtnofac1  41482  prmdvdsfmtnof1lem1  41496  pwdif  41501  lighneal  41528  sprsymrelfvlem  41740  uspgropssxp  41752  rngccatidALTV  41989  ringccatidALTV  42052  nzerooringczr  42072  lcosslsp  42227  fllog2  42362  dignn0flhalf  42412  iunord  42422  setrec2fun  42439