Theorem 3exp 1152

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

Syntax hints:   -> wi 4   /\ w3a 936

This theorem is referenced by:  3expa  1153  3expb  1154  3expia  1155  3expib  1156  3com23  1159  3an1rs  1165  3exp1  1169  3expd  1170  exp5o  1172  syl3an2  1218  syl3an3  1219  3ecase  1288  3impexpbicomi  1374  rexlimdv3a  2792  rabssdv  3383  reupick2  3587  disjss3  4171  wefrc  4536  tz7.7  4567  unizlim  4657  ssorduni  4725  suceloni  4752  tfisi  4797  sotriOLD  5225  f1oiso2  6031  poxp  6417  riotasv2dOLD  6554  riotasv3dOLD  6558  smo11  6585  odi  6781  omass  6782  nndi  6825  nnmass  6826  undifixp  7057  findcard  7306  ac6sfi  7310  domunfican  7338  fisup2g  7427  indcardi  7878  acndom  7888  ackbij1lem16  8071  infpssrlem4  8142  fin23lem11  8153  isfin2-2  8155  fin23lem34  8182  fin1a2lem10  8245  hsmexlem2  8263  axcc3  8274  domtriomlem  8278  axdc3lem2  8287  axdc3lem4  8289  axcclem  8293  ttukeyg  8353  axdclem2  8356  axacndlem4  8441  axacndlem5  8442  axacnd  8443  tskr1om2  8599  tskwe2  8604  tskord  8611  tskcard  8612  tskuni  8614  tskwun  8615  gruiin  8641  grudomon  8648  gruina  8649  mulcanpi  8733  adderpq  8789  mulerpq  8790  divgt0  9834  divge0  9835  uzind  10317  uzind2  10318  iccsplit  10985  sqlecan  11442  modexp  11469  facavg  11547  pceu  13175  mreexexd  13828  luble  14393  glble  14398  joinle  14405  meetle  14412  clatl  14498  isglbd  14499  mulgass2  15665  islss4  15993  lspsneu  16150  lspfixed  16155  lspexch  16156  lsmcv  16168  lspsolvlem  16169  xrsdsreclblem  16699  isphld  16840  fiinopn  16929  neips  17132  tpnei  17140  neindisj2  17142  opnneiid  17145  hausnei2  17371  cmpsublem  17416  cmpsub  17417  cmpcld  17419  filufint  17905  cfinufil  17913  rnelfm  17938  alexsubALTlem1  18031  alexsubALTlem4  18034  alexsubALT  18035  tsmsxp  18137  neibl  18484  tgqioo  18784  ovolunlem2  19347  iunmbl2  19404  itg1le  19558  vieta1  20182  aannenlem2  20199  aalioulem3  20204  aalioulem4  20205  aaliou2  20210  wilthlem3  20806  bcmono  21014  usgrafisinds  21380  cusgrasize2inds  21439  1pthoncl  21545  wlkdvspth  21561  nvnencycllem  21583  gxid  21814  gxdi  21837  clmgm  21862  grpomndo  21887  zerdivemp1  21975  chintcli  22786  spansnss  23026  elspansn4  23028  chscllem4  23095  hoadddir  23260  adjmul  23548  kbass6  23577  stadd3i  23704  spansncv2  23749  sumdmdii  23871  dedekindle  25141  prodfn0  25175  prodfrec  25176  ntrivcvgfvn0  25180  fprodabs  25250  fprodefsum  25251  iprodefisumlem  25270  predpo  25398  poseq  25467  axcontlem7  25813  btwndiff  25865  bpolycl  26002  bpolydif  26005  elicc3  26210  finminlem  26211  comppfsc  26277  sdclem2  26336  zerdivemp1x  26461  mzpexpmpt  26692  pellexlem5  26786  pellex  26788  pell14qrexpclnn0  26819  pellfundex  26839  monotuz  26894  monotoddzzfi  26895  expmordi  26900  rmxypos  26902  jm2.17a  26915  jm2.17b  26916  rmygeid  26919  jm2.19lem3  26952  jm2.15nn0  26964  jm2.16nn0  26965  aomclem2  27020  aomclem6  27024  dfac11  27028  mapfien2  27126  hbtlem5  27200  cnsrexpcl  27238  pmtrfrn  27268  psgnunilem4  27288  refsumcn  27568  fmul01  27577  fmuldfeq  27580  fmul01lt1  27583  stoweidlem3  27619  stoweidlem31  27647  stoweidlem59  27675  stirlinglem13  27702  n4cyclfrgra  28122  vdgfrgragt2  28132  ad4ant123  28254  ad4ant124  28255  ad4ant134  28256  ad4ant234  28259  ad5ant245  28267  ad5ant234  28268  ad5ant235  28269  ad5ant123  28270  ad5ant124  28271  ad5ant125  28272  ad5ant134  28273  ad5ant135  28274  ad5ant145  28275  ee333  28300  eel2221  28513  eel12131  28530  eel32131  28533  eel2122old  28537  e333  28554  ordelordALTVD  28688  bnj1417  29116  lsmsat  29491  lsmcv2  29512  lcvat  29513  lsatcveq0  29515  lcvexchlem4  29520  lcvexchlem5  29521  islshpcv  29536  l1cvpat  29537  lshpkrlem6  29598  omlfh3N  29742  cvlsupr4  29828  cvlsupr5  29829  cvlsupr6  29830  2llnneN  29891  hlrelat3  29894  cvrval3  29895  cvrval4N  29896  cvrexchlem  29901  2atlt  29921  cvrat4  29925  atbtwnexOLDN  29929  atbtwnex  29930  athgt  29938  3dim1  29949  3dim2  29950  3dim3  29951  1cvratex  29955  llnle  30000  atcvrlln2  30001  atcvrlln  30002  2llnmat  30006  lplnle  30022  lplnnle2at  30023  lplnnlelln  30025  llncvrlpln2  30039  2llnjN  30049  lvoli2  30063  lvolnlelln  30066  lvolnlelpln  30067  4atlem10  30088  4atlem11  30091  4atlem12  30094  lplncvrlvol2  30097  2lplnj  30102  lneq2at  30260  lnatexN  30261  lnjatN  30262  lncvrat  30264  2lnat  30266  cdlemb  30276  paddasslem14  30315  llnexchb2  30351  dalawlem10  30362  dalawlem13  30365  dalawlem14  30366  dalaw  30368  pclclN  30373  pclfinN  30382  osumcllem11N  30448  lhp2lt  30483  lhpexle3lem  30493  4atexlem7  30557  ldilcnv  30597  ldilco  30598  ltrncnv  30628  trlval2  30645  cdleme24  30834  cdleme26ee  30842  cdleme28  30855  cdleme32le  30929  cdleme50trn2  31033  cdleme50ltrn  31039  cdleme  31042  cdlemf1  31043  cdlemf  31045  cdlemg1cex  31070  cdlemg2ce  31074  cdlemg18b  31161  ltrnco  31201  tendocan  31306  cdlemk28-3  31390  cdlemk11t  31428  dia2dimlem6  31552  dia2dimlem12  31558  dihlsscpre  31717  dihord4  31741  dihord5b  31742  dihmeetlem3N  31788  dihmeetlem20N  31809  dvh4dimlem  31926  lclkrlem2y  32014  mapdpglem24  32187  mapdpglem32  32188  mapdpg  32189  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195  mapdh9a  32273  mapdh9aOLDN  32274  hdmap14lem6  32359  hdmapglem7  32415

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938