Theorem 3exp 1193

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 1173	. 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 971

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 369  df-3an 973

This theorem is referenced by:  3expa  1194  3expb  1195  3expia  1196  3expib  1197  3com23  1200  3an1rs  1206  3exp1  1210  3expd  1211  exp5o  1213  syl3an2  1260  syl3an3  1261  3ecase  1331  rexlimdv3a  2948  rabssdv  3566  reupick2  3781  disjss3  4438  wefrc  4862  tz7.7  4893  unizlim  4983  fveqdmss  6002  f1oiso2  6223  ssorduni  6594  suceloni  6621  tfisi  6666  poxp  6885  smo11  7027  tfrlem5  7041  odi  7220  omass  7221  nndi  7264  nnmass  7265  undifixp  7498  findcard  7751  ac6sfi  7756  domunfican  7785  mapfien2  7860  fisup2g  7918  indcardi  8413  acndom  8423  ackbij1lem16  8606  infpssrlem4  8677  fin23lem11  8688  isfin2-2  8690  fin23lem34  8717  fin1a2lem10  8780  hsmexlem2  8798  axcc3  8809  domtriomlem  8813  axdc3lem2  8822  axdc3lem4  8824  axcclem  8828  ttukeyg  8888  axdclem2  8891  axacndlem4  8977  axacndlem5  8978  axacnd  8979  tskr1om2  9135  tskwe2  9140  tskord  9147  tskcard  9148  tskuni  9150  tskwun  9151  gruiin  9177  grudomon  9184  gruina  9185  mulcanpi  9267  adderpq  9323  mulerpq  9324  dedekindle  9734  divgt0  10406  divge0  10407  uzind  10950  uzind2  10951  iccsplit  11656  ssnn0fi  12076  sqlecan  12256  modexp  12283  facavg  12361  2cshwcshw  12784  relexpcnv  12950  relexpreld  12955  relexpaddnn  12966  relexpaddg  12968  prodfn0  13785  prodfrec  13786  ntrivcvgfvn0  13790  fprodabs  13860  fprodefsum  13912  pceu  14454  mreexexd  15137  initoeu1  15489  termoeu1  15496  isglbd  15946  pmtrfrn  16682  psgnunilem4  16721  mulgass2  17442  islss4  17803  lspsneu  17964  lspfixed  17969  lspexch  17970  lsmcv  17982  lspsolvlem  17983  xrsdsreclblem  18659  isphld  18862  mdetralt  19277  mdetunilem9  19289  fiinopn  19577  neips  19781  tpnei  19789  neindisj2  19791  opnneiid  19794  hausnei2  20021  cmpsublem  20066  cmpsub  20067  cmpcld  20069  comppfsc  20199  filufint  20587  cfinufil  20595  rnelfm  20620  alexsubALTlem1  20713  alexsubALTlem4  20716  alexsubALT  20717  tsmsxp  20823  neibl  21170  tgqioo  21471  ovolunlem2  22075  iunmbl2  22133  itg1le  22286  vieta1  22874  aannenlem2  22891  aalioulem3  22896  aalioulem4  22897  aaliou2  22902  wilthlem3  23542  bcmono  23750  axcontlem7  24475  usgrafisinds  24615  cusgrasize2inds  24679  1pthoncl  24796  wlkdvspth  24812  nvnencycllem  24845  wwlknred  24925  wwlknextbi  24927  clwlkfclwwlk  25046  cusgraiffrusgra  25142  n4cyclfrgra  25220  vdgfrgragt2  25229  usgn0fidegnn0  25231  frgraregord013  25320  gxid  25473  gxdi  25496  clmgmOLD  25521  grpomndo  25546  zerdivemp1  25634  chintcli  26447  spansnss  26687  elspansn4  26689  chscllem4  26756  hoadddir  26921  adjmul  27209  kbass6  27238  stadd3i  27365  spansncv2  27410  sumdmdii  27532  nexple  28239  mclsind  29194  iprodefisumlem  29364  predpo  29504  poseq  29573  btwndiff  29905  bpolycl  30042  bpolydif  30045  elicc3  30375  finminlem  30376  sdclem2  30475  zerdivemp1x  30598  mzpexpmpt  30917  pellexlem5  31008  pellex  31010  pell14qrexpclnn0  31041  pellfundex  31061  monotuz  31116  monotoddzzfi  31117  expmordi  31122  rmxypos  31124  jm2.17a  31137  jm2.17b  31138  rmygeid  31141  jm2.19lem3  31172  jm2.15nn0  31184  jm2.16nn0  31185  aomclem2  31240  aomclem6  31244  dfac11  31247  mapfien2OLD  31281  hbtlem5  31318  cnsrexpcl  31355  refsumcn  31645  suprnmpt  31691  fperiodmullem  31742  upbdrech  31744  ssfiunibd  31748  iccshift  31797  iooshift  31801  fmul01  31813  fmuldfeq  31816  fmul01lt1  31819  fprodle  31843  mullimc  31861  islptre  31864  mullimcf  31868  limcperiod  31873  islpcn  31884  limsupre  31886  limcleqr  31889  neglimc  31892  addlimc  31893  0ellimcdiv  31894  limclner  31896  coskpi2  31905  cosknegpi  31908  cncfshift  31915  cncfperiod  31920  icccncfext  31929  dvnmptdivc  31974  dvnmptconst  31977  dvnmul  31979  dvmptfprodlem  31980  dvmptfprod  31981  dvnprodlem1  31982  dvnprodlem2  31983  iblspltprt  32011  itgspltprt  32017  itgperiod  32019  stoweidlem3  32024  stoweidlem31  32052  stoweidlem59  32080  stirlinglem13  32107  fourierdlem41  32169  fourierdlem42  32170  fourierdlem48  32176  fourierdlem51  32179  fourierdlem53  32181  fourierdlem70  32198  fourierdlem71  32199  fourierdlem73  32201  fourierdlem80  32208  fourierdlem81  32209  fourierdlem89  32217  fourierdlem91  32219  fourierdlem93  32221  fourierdlem97  32225  elaa2  32256  uhgrauhgbi  32746  rngccatidALTV  33051  ringccatidALTV  33114  nzerooringczr  33134  lcosslsp  33293  fllog2  33443  dignn0flhalf  33493  3impexpbicomi  33609  ad4ant123  33613  ad4ant124  33614  ad4ant134  33615  ad4ant234  33618  ad5ant245  33626  ad5ant234  33627  ad5ant235  33628  ad5ant123  33629  ad5ant124  33630  ad5ant125  33631  ad5ant134  33632  ad5ant135  33633  ad5ant145  33634  ee333  33663  eel2221  33883  eel12131  33900  eel32131  33903  eel2122old  33907  e333  33924  ordelordALTVD  34068  bnj1417  34498  lsmsat  35130  lsmcv2  35151  lcvat  35152  lsatcveq0  35154  lcvexchlem4  35159  lcvexchlem5  35160  islshpcv  35175  l1cvpat  35176  lshpkrlem6  35237  omlfh3N  35381  cvlsupr4  35467  cvlsupr5  35468  cvlsupr6  35469  2llnneN  35530  hlrelat3  35533  cvrval3  35534  cvrval4N  35535  cvrexchlem  35540  2atlt  35560  cvrat4  35564  atbtwnexOLDN  35568  atbtwnex  35569  athgt  35577  3dim1  35588  3dim2  35589  3dim3  35590  1cvratex  35594  llnle  35639  atcvrlln2  35640  atcvrlln  35641  2llnmat  35645  lplnle  35661  lplnnle2at  35662  lplnnlelln  35664  llncvrlpln2  35678  2llnjN  35688  lvoli2  35702  lvolnlelln  35705  lvolnlelpln  35706  4atlem10  35727  4atlem11  35730  4atlem12  35733  lplncvrlvol2  35736  2lplnj  35741  lneq2at  35899  lnatexN  35900  lnjatN  35901  lncvrat  35903  2lnat  35905  cdlemb  35915  paddasslem14  35954  llnexchb2  35990  dalawlem10  36001  dalawlem13  36004  dalawlem14  36005  dalaw  36007  pclclN  36012  pclfinN  36021  osumcllem11N  36087  lhp2lt  36122  lhpexle3lem  36132  4atexlem7  36196  ldilcnv  36236  ldilco  36237  ltrncnv  36267  trlval2  36285  cdleme24  36475  cdleme26ee  36483  cdleme28  36496  cdleme32le  36570  cdleme50trn2  36674  cdleme50ltrn  36680  cdleme  36683  cdlemf1  36684  cdlemf  36686  cdlemg1cex  36711  cdlemg2ce  36715  cdlemg18b  36802  ltrnco  36842  tendocan  36947  cdlemk28-3  37031  cdlemk11t  37069  dia2dimlem6  37193  dia2dimlem12  37199  dihlsscpre  37358  dihord4  37382  dihord5b  37383  dihmeetlem3N  37429  dihmeetlem20N  37450  dvh4dimlem  37567  lclkrlem2y  37655  mapdpglem24  37828  mapdpglem32  37829  mapdpg  37830  baerlem3lem2  37834  baerlem5alem2  37835  baerlem5blem2  37836  mapdh9a  37914  mapdh9aOLDN  37915  hdmap14lem6  38000  hdmapglem7  38056  relexpaddss  38205  iunrelexpmin1  38207  iunrelexpmin2  38208  relexpss1d  38217  relexp01min  38219  relexpiidm  38222  relexp0a  38223  relexpxpnnidm  38225  relexpxpmin  38226  relexpmulnn  38227