Theorem 3exp 1195

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 1175	. 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 973

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 975

This theorem is referenced by:  3expa  1196  3expb  1197  3expia  1198  3expib  1199  3com23  1202  3an1rs  1208  3exp1  1212  3expd  1213  exp5o  1215  syl3an2  1262  syl3an3  1263  3ecase  1333  rexlimdv3a  2957  rabssdv  3580  reupick2  3784  disjss3  4446  wefrc  4873  tz7.7  4904  unizlim  4994  sotriOLD  5397  f1oiso2  6234  ssorduni  6599  suceloni  6626  tfisi  6671  poxp  6892  smo11  7032  tfrlem5  7046  odi  7225  omass  7226  nndi  7269  nnmass  7270  undifixp  7502  findcard  7755  ac6sfi  7760  domunfican  7789  mapfien2  7864  fisup2g  7922  indcardi  8418  acndom  8428  ackbij1lem16  8611  infpssrlem4  8682  fin23lem11  8693  isfin2-2  8695  fin23lem34  8722  fin1a2lem10  8785  hsmexlem2  8803  axcc3  8814  domtriomlem  8818  axdc3lem2  8827  axdc3lem4  8829  axcclem  8833  ttukeyg  8893  axdclem2  8896  axacndlem4  8984  axacndlem5  8985  axacnd  8986  tskr1om2  9142  tskwe2  9147  tskord  9154  tskcard  9155  tskuni  9157  tskwun  9158  gruiin  9184  grudomon  9191  gruina  9192  mulcanpi  9274  adderpq  9330  mulerpq  9331  dedekindle  9740  divgt0  10406  divge0  10407  uzind  10948  uzind2  10949  iccsplit  11649  ssnn0fi  12058  sqlecan  12238  modexp  12265  facavg  12343  2cshwcshw  12752  pceu  14225  mreexexd  14899  isglbd  15600  pmtrfrn  16279  psgnunilem4  16318  mulgass2  17033  islss4  17391  lspsneu  17552  lspfixed  17557  lspexch  17558  lsmcv  17570  lspsolvlem  17571  xrsdsreclblem  18232  isphld  18456  mdetralt  18877  mdetunilem9  18889  fiinopn  19177  neips  19380  tpnei  19388  neindisj2  19390  opnneiid  19393  hausnei2  19620  cmpsublem  19665  cmpsub  19666  cmpcld  19668  bwthOLD  19677  filufint  20156  cfinufil  20164  rnelfm  20189  alexsubALTlem1  20282  alexsubALTlem4  20285  alexsubALT  20286  tsmsxp  20392  neibl  20739  tgqioo  21040  ovolunlem2  21644  iunmbl2  21702  itg1le  21855  vieta1  22442  aannenlem2  22459  aalioulem3  22464  aalioulem4  22465  aaliou2  22470  wilthlem3  23072  bcmono  23280  axcontlem7  23949  usgrafisinds  24089  cusgrasize2inds  24153  1pthoncl  24270  wlkdvspth  24286  nvnencycllem  24319  wwlknred  24399  wwlknextbi  24401  clwlkfclwwlk  24520  cusgraiffrusgra  24616  n4cyclfrgra  24694  vdgfrgragt2  24704  usgn0fidegnn0  24706  frgraregord013  24795  gxid  24951  gxdi  24974  clmgm  24999  grpomndo  25024  zerdivemp1  25112  chintcli  25925  spansnss  26165  elspansn4  26167  chscllem4  26234  hoadddir  26399  adjmul  26687  kbass6  26716  stadd3i  26843  spansncv2  26888  sumdmdii  27010  prodfn0  28605  prodfrec  28606  ntrivcvgfvn0  28610  fprodabs  28680  fprodefsum  28681  iprodefisumlem  28700  predpo  28841  poseq  28910  btwndiff  29254  bpolycl  29391  bpolydif  29394  elicc3  29712  finminlem  29713  comppfsc  29779  sdclem2  29838  zerdivemp1x  29961  mzpexpmpt  30281  pellexlem5  30373  pellex  30375  pell14qrexpclnn0  30406  pellfundex  30426  monotuz  30481  monotoddzzfi  30482  expmordi  30487  rmxypos  30489  jm2.17a  30502  jm2.17b  30503  rmygeid  30506  jm2.19lem3  30537  jm2.15nn0  30549  jm2.16nn0  30550  aomclem2  30605  aomclem6  30609  dfac11  30612  mapfien2OLD  30646  hbtlem5  30681  cnsrexpcl  30719  refsumcn  30983  suprnmpt  31029  fperiodmullem  31080  upbdrech  31082  ssfiunibd  31086  iccshift  31122  iooshift  31126  fmul01  31130  fmuldfeq  31133  fmul01lt1  31136  mullimc  31158  islptre  31161  limccog  31162  mullimcf  31165  limcperiod  31170  islpcn  31181  limsupre  31183  limcleqr  31186  neglimc  31189  addlimc  31190  0ellimcdiv  31191  limclner  31193  coskpi2  31202  cosknegpi  31205  cncfshift  31212  cncfperiod  31217  cncfuni  31225  icccncfext  31226  dvbdfbdioolem1  31258  iblspltprt  31291  itgspltprt  31297  itgiccshift  31298  itgperiod  31299  stoweidlem3  31303  stoweidlem31  31331  stoweidlem59  31359  stirlinglem13  31386  fourierdlem41  31448  fourierdlem42  31449  fourierdlem48  31455  fourierdlem49  31456  fourierdlem51  31458  fourierdlem52  31459  fourierdlem53  31460  fourierdlem54  31461  fourierdlem68  31475  fourierdlem70  31477  fourierdlem71  31478  fourierdlem73  31480  fourierdlem77  31484  fourierdlem80  31487  fourierdlem81  31488  fourierdlem83  31490  fourierdlem87  31494  fourierdlem89  31496  fourierdlem91  31498  fourierdlem93  31500  fourierdlem97  31504  fourierdlem102  31509  fourierdlem103  31510  fourierdlem104  31511  fourierdlem113  31520  fourierdlem114  31521  uhgrauhgbi  31843  lcosslsp  32112  3impexpbicomi  32301  ad4ant123  32305  ad4ant124  32306  ad4ant134  32307  ad4ant234  32310  ad5ant245  32318  ad5ant234  32319  ad5ant235  32320  ad5ant123  32321  ad5ant124  32322  ad5ant125  32323  ad5ant134  32324  ad5ant135  32325  ad5ant145  32326  ee333  32355  eel2221  32569  eel12131  32586  eel32131  32589  eel2122old  32593  e333  32610  ordelordALTVD  32747  bnj1417  33176  lsmsat  33805  lsmcv2  33826  lcvat  33827  lsatcveq0  33829  lcvexchlem4  33834  lcvexchlem5  33835  islshpcv  33850  l1cvpat  33851  lshpkrlem6  33912  omlfh3N  34056  cvlsupr4  34142  cvlsupr5  34143  cvlsupr6  34144  2llnneN  34205  hlrelat3  34208  cvrval3  34209  cvrval4N  34210  cvrexchlem  34215  2atlt  34235  cvrat4  34239  atbtwnexOLDN  34243  atbtwnex  34244  athgt  34252  3dim1  34263  3dim2  34264  3dim3  34265  1cvratex  34269  llnle  34314  atcvrlln2  34315  atcvrlln  34316  2llnmat  34320  lplnle  34336  lplnnle2at  34337  lplnnlelln  34339  llncvrlpln2  34353  2llnjN  34363  lvoli2  34377  lvolnlelln  34380  lvolnlelpln  34381  4atlem10  34402  4atlem11  34405  4atlem12  34408  lplncvrlvol2  34411  2lplnj  34416  lneq2at  34574  lnatexN  34575  lnjatN  34576  lncvrat  34578  2lnat  34580  cdlemb  34590  paddasslem14  34629  llnexchb2  34665  dalawlem10  34676  dalawlem13  34679  dalawlem14  34680  dalaw  34682  pclclN  34687  pclfinN  34696  osumcllem11N  34762  lhp2lt  34797  lhpexle3lem  34807  4atexlem7  34871  ldilcnv  34911  ldilco  34912  ltrncnv  34942  trlval2  34959  cdleme24  35148  cdleme26ee  35156  cdleme28  35169  cdleme32le  35243  cdleme50trn2  35347  cdleme50ltrn  35353  cdleme  35356  cdlemf1  35357  cdlemf  35359  cdlemg1cex  35384  cdlemg2ce  35388  cdlemg18b  35475  ltrnco  35515  tendocan  35620  cdlemk28-3  35704  cdlemk11t  35742  dia2dimlem6  35866  dia2dimlem12  35872  dihlsscpre  36031  dihord4  36055  dihord5b  36056  dihmeetlem3N  36102  dihmeetlem20N  36123  dvh4dimlem  36240  lclkrlem2y  36328  mapdpglem24  36501  mapdpglem32  36502  mapdpg  36503  baerlem3lem2  36507  baerlem5alem2  36508  baerlem5blem2  36509  mapdh9a  36587  mapdh9aOLDN  36588  hdmap14lem6  36673  hdmapglem7  36729