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

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

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  2926  rabssdv  3547  reupick2  3765  disjss3  4425  wefrc  4848  predpo  5417  tz7.7  5468  unizlim  5558  fveqdmss  6032  f1oiso2  6258  ssorduni  6626  suceloni  6654  tfisi  6699  poxp  6919  smo11  7091  tfrlem5  7106  odi  7288  omass  7289  nndi  7332  nnmass  7333  undifixp  7566  findcard  7816  ac6sfi  7821  domunfican  7850  mapfien2  7928  fisup2g  7990  indcardi  8470  acndom  8480  ackbij1lem16  8663  infpssrlem4  8734  fin23lem11  8745  isfin2-2  8747  fin23lem34  8774  fin1a2lem10  8837  hsmexlem2  8855  axcc3  8866  domtriomlem  8870  axdc3lem2  8879  axdc3lem4  8881  axcclem  8885  ttukeyg  8945  axdclem2  8948  axacndlem4  9034  axacndlem5  9035  axacnd  9036  tskr1om2  9192  tskwe2  9197  tskord  9204  tskcard  9205  tskuni  9207  tskwun  9208  gruiin  9234  grudomon  9241  gruina  9242  mulcanpi  9324  adderpq  9380  mulerpq  9381  dedekindle  9797  divgt0  10472  divge0  10473  uzind  11027  uzind2  11028  iccsplit  11763  ssnn0fi  12194  sqlecan  12378  modexp  12404  facavg  12483  2cshwcshw  12909  relexpcnv  13077  relexpreld  13082  relexpaddnn  13093  relexpaddg  13095  prodfn0  13928  prodfrec  13929  ntrivcvgfvn0  13933  fprodabs  14006  fprodle  14028  bpolycl  14083  bpolydif  14086  fprodefsum  14127  ncoprmlnprm  14648  pceu  14759  mreexexd  15505  initoeu1  15857  termoeu1  15864  isglbd  16314  pmtrfrn  17050  psgnunilem4  17089  mulgass2  17764  islss4  18120  lspsneu  18281  lspfixed  18286  lspexch  18287  lsmcv  18299  lspsolvlem  18300  xrsdsreclblem  18949  isphld  19152  mdetralt  19564  mdetunilem9  19576  fiinopn  19862  neips  20060  tpnei  20068  neindisj2  20070  opnneiid  20073  hausnei2  20300  cmpsublem  20345  cmpsub  20346  cmpcld  20348  comppfsc  20478  filufint  20866  cfinufil  20874  rnelfm  20899  alexsubALTlem1  20993  alexsubALTlem4  20996  alexsubALT  20997  tsmsxp  21100  neibl  21447  tgqioo  21729  ovolunlem2  22329  iunmbl2  22387  itg1le  22548  vieta1  23133  aannenlem2  23150  aalioulem3  23155  aalioulem4  23156  aaliou2  23161  wilthlem3  23860  bcmono  24068  axcontlem7  24846  usgrafisinds  24986  cusgrasize2inds  25050  1pthoncl  25167  wlkdvspth  25183  nvnencycllem  25216  wwlknred  25296  wwlknextbi  25298  clwlkfclwwlk  25417  cusgraiffrusgra  25513  n4cyclfrgra  25591  vdgfrgragt2  25600  usgn0fidegnn0  25602  frgraregord013  25691  gxid  25846  gxdi  25869  clmgmOLD  25894  grpomndo  25919  zerdivemp1  26007  chintcli  26819  spansnss  27059  elspansn4  27061  chscllem4  27128  hoadddir  27292  adjmul  27580  kbass6  27609  stadd3i  27736  spansncv2  27781  sumdmdii  27903  nexple  28670  bnj1417  29638  mclsind  29996  iprodefisumlem  30163  poseq  30278  btwndiff  30579  elicc3  30758  finminlem  30759  sdclem2  31775  zerdivemp1x  31898  lsmsat  32283  lsmcv2  32304  lcvat  32305  lsatcveq0  32307  lcvexchlem4  32312  lcvexchlem5  32313  islshpcv  32328  l1cvpat  32329  lshpkrlem6  32390  omlfh3N  32534  cvlsupr4  32620  cvlsupr5  32621  cvlsupr6  32622  2llnneN  32683  hlrelat3  32686  cvrval3  32687  cvrval4N  32688  cvrexchlem  32693  2atlt  32713  cvrat4  32717  atbtwnexOLDN  32721  atbtwnex  32722  athgt  32730  3dim1  32741  3dim2  32742  3dim3  32743  1cvratex  32747  llnle  32792  atcvrlln2  32793  atcvrlln  32794  2llnmat  32798  lplnle  32814  lplnnle2at  32815  lplnnlelln  32817  llncvrlpln2  32831  2llnjN  32841  lvoli2  32855  lvolnlelln  32858  lvolnlelpln  32859  4atlem10  32880  4atlem11  32883  4atlem12  32886  lplncvrlvol2  32889  2lplnj  32894  lneq2at  33052  lnatexN  33053  lnjatN  33054  lncvrat  33056  2lnat  33058  cdlemb  33068  paddasslem14  33107  llnexchb2  33143  dalawlem10  33154  dalawlem13  33157  dalawlem14  33158  dalaw  33160  pclclN  33165  pclfinN  33174  osumcllem11N  33240  lhp2lt  33275  lhpexle3lem  33285  4atexlem7  33349  ldilcnv  33389  ldilco  33390  ltrncnv  33420  trlval2  33438  cdleme24  33628  cdleme26ee  33636  cdleme28  33649  cdleme32le  33723  cdleme50trn2  33827  cdleme50ltrn  33833  cdleme  33836  cdlemf1  33837  cdlemf  33839  cdlemg1cex  33864  cdlemg2ce  33868  cdlemg18b  33955  ltrnco  33995  tendocan  34100  cdlemk28-3  34184  cdlemk11t  34222  dia2dimlem6  34346  dia2dimlem12  34352  dihlsscpre  34511  dihord4  34535  dihord5b  34536  dihmeetlem3N  34582  dihmeetlem20N  34603  dvh4dimlem  34720  lclkrlem2y  34808  mapdpglem24  34981  mapdpglem32  34982  mapdpg  34983  baerlem3lem2  34987  baerlem5alem2  34988  baerlem5blem2  34989  mapdh9a  35067  mapdh9aOLDN  35068  hdmap14lem6  35153  hdmapglem7  35209  mzpexpmpt  35296  pellexlem5  35387  pellex  35389  pell14qrexpclnn0  35420  pellfundex  35440  monotuz  35495  monotoddzzfi  35496  expmordi  35501  rmxypos  35503  jm2.17a  35516  jm2.17b  35517  rmygeid  35520  jm2.19lem3  35552  jm2.15nn0  35564  jm2.16nn0  35565  aomclem2  35619  aomclem6  35623  dfac11  35626  hbtlem5  35693  cnsrexpcl  35730  relexpxpnnidm  35934  relexpiidm  35935  relexpss1d  35936  iunrelexpmin1  35939  relexpmulnn  35940  iunrelexpmin2  35943  relexp01min  35944  relexp0a  35947  relexpxpmin  35948  relexpaddss  35949  trclimalb2  35957  3impexpbicomi  36472  ee333  36500  eel2221  36720  eel12131  36737  eel32131  36740  eel2122old  36743  e333  36760  ordelordALTVD  36904  refsumcn  36991  uzwo4  37033  suprnmpt  37061  wessf1ornlem  37082  disjf1o  37089  fompt  37090  disjinfi  37091  fperiodmullem  37130  upbdrech  37132  ssfiunibd  37136  supxrgere  37165  iuneqfzuzlem  37166  supxrgelem  37169  supxrge  37170  suplesup  37171  iccshift  37204  iooshift  37208  fmul01  37230  fmuldfeq  37233  fmul01lt1  37236  mullimc  37268  islptre  37271  mullimcf  37275  limcperiod  37280  islpcn  37291  limsupre  37293  limsupreOLD  37294  limcleqr  37297  neglimc  37300  addlimc  37301  0ellimcdiv  37302  limclner  37304  coskpi2  37313  cosknegpi  37316  cncfshift  37323  cncfperiod  37328  icccncfext  37337  dvnmptdivc  37382  dvnmptconst  37385  dvnmul  37387  dvmptfprodlem  37388  dvmptfprod  37389  dvnprodlem1  37390  dvnprodlem2  37391  iblspltprt  37419  itgspltprt  37425  itgperiod  37427  stoweidlem3  37432  stoweidlem31  37461  stoweidlem59  37489  stirlinglem13  37517  fourierdlem41  37579  fourierdlem42  37580  fourierdlem48  37586  fourierdlem51  37589  fourierdlem53  37591  fourierdlem70  37608  fourierdlem71  37609  fourierdlem73  37611  fourierdlem80  37618  fourierdlem81  37619  fourierdlem89  37627  fourierdlem91  37629  fourierdlem93  37631  fourierdlem97  37635  elaa2  37666  sge0tsms  37756  sge0f1o  37758  sge0fsum  37763  sge0supre  37765  sge0sup  37767  sge0rnbnd  37769  sge0gerp  37771  sge0pnffigt  37772  sge0lefi  37774  sge0ltfirp  37776  sge0resrn  37780  sge0resplit  37782  sge0split  37785  sge0iunmptlemfi  37789  sge0iunmptlemre  37791  sge0iunmpt  37794  nnfoctbdjlem  37802  nnfoctbdj  37803  iundjiun  37807  meadjiunlem  37812  carageniuncllem1  37851  carageniuncllem2  37852  caratheodorylem1  37856  caratheodorylem2  37857  iccpartiltu  38126  uhgrauhgbi  38444  rngccatidALTV  38749  ringccatidALTV  38812  nzerooringczr  38832  lcosslsp  38991  fllog2  39140  dignn0flhalf  39190