Theorem 3exp 1214

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 1193	. 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 991

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 190  df-an 377  df-3an 993

This theorem is referenced by:  3expa  1215  3expb  1216  3expia  1217  3expib  1218  3com23  1221  3imp3i2an  1228  3an1rs  1229  3exp1  1233  3expd  1234  exp5o  1236  ad4ant123  1244  ad4ant124  1245  ad4ant134  1246  ad4ant234  1249  ad5ant245  1257  ad5ant234  1258  ad5ant235  1259  ad5ant123  1260  ad5ant124  1261  ad5ant125  1262  ad5ant134  1263  ad5ant135  1264  ad5ant145  1265  syl3an2  1310  syl3an3  1311  3ecase  1384  rexlimdv3a  2893  rabssdv  3521  reupick2  3741  disjss3  4415  wefrc  4847  predpo  5417  tz7.7  5468  unizlim  5558  fveqdmss  6040  f1oiso2  6268  ssorduni  6639  suceloni  6667  tfisi  6712  poxp  6935  smo11  7109  tfrlem5  7124  odi  7306  omass  7307  nndi  7350  nnmass  7351  undifixp  7584  findcard  7836  ac6sfi  7841  domunfican  7870  mapfien2  7948  fisup2g  8010  fiinf2g  8042  indcardi  8498  acndom  8508  ackbij1lem16  8691  infpssrlem4  8762  fin23lem11  8773  isfin2-2  8775  fin23lem34  8802  fin1a2lem10  8865  hsmexlem2  8883  axcc3  8894  domtriomlem  8898  axdc3lem2  8907  axdc3lem4  8909  axcclem  8913  ttukeyg  8973  axdclem2  8976  axacndlem4  9061  axacndlem5  9062  axacnd  9063  tskr1om2  9219  tskwe2  9224  tskord  9231  tskcard  9232  tskuni  9234  tskwun  9235  gruiin  9261  grudomon  9268  gruina  9269  mulcanpi  9351  adderpq  9407  mulerpq  9408  dedekindle  9824  divgt0  10501  divge0  10502  uzind  11056  uzind2  11057  iccsplit  11794  ssnn0fi  12229  sqlecan  12413  modexp  12439  facavg  12518  2cshwcshw  12961  relexpcnv  13147  relexpreld  13152  relexpaddnn  13163  relexpaddg  13165  prodfn0  13999  prodfrec  14000  ntrivcvgfvn0  14004  fprodabs  14077  fprodle  14099  bpolycl  14154  bpolydif  14157  fprodefsum  14198  ncoprmlnprm  14726  pceu  14845  mreexexd  15603  initoeu1  15955  termoeu1  15962  isglbd  16412  pmtrfrn  17148  psgnunilem4  17187  mulgass2  17878  islss4  18234  lspsneu  18395  lspfixed  18400  lspexch  18401  lsmcv  18413  lspsolvlem  18414  xrsdsreclblem  19063  isphld  19270  mdetralt  19682  mdetunilem9  19694  fiinopn  19980  neips  20178  tpnei  20186  neindisj2  20188  opnneiid  20191  hausnei2  20418  cmpsublem  20463  cmpsub  20464  cmpcld  20466  comppfsc  20596  filufint  20984  cfinufil  20992  rnelfm  21017  alexsubALTlem1  21111  alexsubALTlem4  21114  alexsubALT  21115  tsmsxp  21218  neibl  21565  tgqioo  21867  ovolunlem2  22500  iunmbl2  22559  itg1le  22720  vieta1  23314  aannenlem2  23334  aalioulem3  23339  aalioulem4  23340  aaliou2  23345  wilthlem3  24044  bcmono  24254  axcontlem7  25049  usgrafisinds  25190  cusgrasize2inds  25254  1pthoncl  25371  wlkdvspth  25387  nvnencycllem  25420  wwlknred  25500  wwlknextbi  25502  clwlkfclwwlk  25621  cusgraiffrusgra  25717  n4cyclfrgra  25795  vdgfrgragt2  25804  usgn0fidegnn0  25806  frgraregord013  25895  gxid  26050  gxdi  26073  clmgmOLD  26098  grpomndo  26123  zerdivemp1  26211  chintcli  27033  spansnss  27273  elspansn4  27275  chscllem4  27342  hoadddir  27506  adjmul  27794  kbass6  27823  stadd3i  27950  spansncv2  27995  sumdmdii  28117  nexple  28880  bnj1417  29899  mclsind  30257  iprodefisumlem  30425  poseq  30540  btwndiff  30843  elicc3  31022  finminlem  31023  sdclem2  32116  zerdivemp1x  32239  lsmsat  32619  lsmcv2  32640  lcvat  32641  lsatcveq0  32643  lcvexchlem4  32648  lcvexchlem5  32649  islshpcv  32664  l1cvpat  32665  lshpkrlem6  32726  omlfh3N  32870  cvlsupr4  32956  cvlsupr5  32957  cvlsupr6  32958  2llnneN  33019  hlrelat3  33022  cvrval3  33023  cvrval4N  33024  cvrexchlem  33029  2atlt  33049  cvrat4  33053  atbtwnexOLDN  33057  atbtwnex  33058  athgt  33066  3dim1  33077  3dim2  33078  3dim3  33079  1cvratex  33083  llnle  33128  atcvrlln2  33129  atcvrlln  33130  2llnmat  33134  lplnle  33150  lplnnle2at  33151  lplnnlelln  33153  llncvrlpln2  33167  2llnjN  33177  lvoli2  33191  lvolnlelln  33194  lvolnlelpln  33195  4atlem10  33216  4atlem11  33219  4atlem12  33222  lplncvrlvol2  33225  2lplnj  33230  lneq2at  33388  lnatexN  33389  lnjatN  33390  lncvrat  33392  2lnat  33394  cdlemb  33404  paddasslem14  33443  llnexchb2  33479  dalawlem10  33490  dalawlem13  33493  dalawlem14  33494  dalaw  33496  pclclN  33501  pclfinN  33510  osumcllem11N  33576  lhp2lt  33611  lhpexle3lem  33621  4atexlem7  33685  ldilcnv  33725  ldilco  33726  ltrncnv  33756  trlval2  33774  cdleme24  33964  cdleme26ee  33972  cdleme28  33985  cdleme32le  34059  cdleme50trn2  34163  cdleme50ltrn  34169  cdleme  34172  cdlemf1  34173  cdlemf  34175  cdlemg1cex  34200  cdlemg2ce  34204  cdlemg18b  34291  ltrnco  34331  tendocan  34436  cdlemk28-3  34520  cdlemk11t  34558  dia2dimlem6  34682  dia2dimlem12  34688  dihlsscpre  34847  dihord4  34871  dihord5b  34872  dihmeetlem3N  34918  dihmeetlem20N  34939  dvh4dimlem  35056  lclkrlem2y  35144  mapdpglem24  35317  mapdpglem32  35318  mapdpg  35319  baerlem3lem2  35323  baerlem5alem2  35324  baerlem5blem2  35325  mapdh9a  35403  mapdh9aOLDN  35404  hdmap14lem6  35489  hdmapglem7  35545  mzpexpmpt  35632  pellexlem5  35722  pellex  35724  pell14qrexpclnn0  35757  pellfundex  35779  monotuz  35834  monotoddzzfi  35835  expmordi  35840  rmxypos  35842  jm2.17a  35855  jm2.17b  35856  rmygeid  35859  jm2.19lem3  35891  jm2.15nn0  35903  jm2.16nn0  35904  aomclem2  35958  aomclem6  35962  dfac11  35965  hbtlem5  36032  cnsrexpcl  36076  relexpxpnnidm  36340  relexpiidm  36341  relexpss1d  36342  iunrelexpmin1  36345  relexpmulnn  36346  iunrelexpmin2  36349  relexp01min  36350  relexp0a  36353  relexpxpmin  36354  relexpaddss  36355  trclimalb2  36363  3impexpbicomi  36879  ee333  36907  eel2221  37125  eel12131  37138  eel2122old  37143  e333  37160  ordelordALTVD  37304  refsumcn  37391  uzwo4  37430  suprnmpt  37477  wessf1ornlem  37497  disjf1o  37504  fompt  37505  disjinfi  37506  ssnnf1octb  37508  mapsnd  37514  choicefi  37519  fperiodmullem  37559  upbdrech  37561  ssfiunibd  37565  supxrgere  37594  iuneqfzuzlem  37595  supxrgelem  37598  supxrge  37599  suplesup  37600  infrpge  37612  iccshift  37657  iooshift  37661  fmul01  37696  fmuldfeq  37699  fmul01lt1  37702  mullimc  37734  islptre  37737  mullimcf  37741  limcperiod  37746  islpcn  37757  limsupre  37759  limsupreOLD  37760  limcleqr  37763  neglimc  37766  addlimc  37767  0ellimcdiv  37768  limclner  37770  coskpi2  37779  cosknegpi  37782  cncfshift  37789  cncfperiod  37794  icccncfext  37803  dvnmptdivc  37851  dvnmptconst  37854  dvnmul  37856  dvmptfprodlem  37857  dvmptfprod  37858  dvnprodlem1  37859  dvnprodlem2  37860  iblspltprt  37888  itgspltprt  37894  itgperiod  37896  stoweidlem3  37901  stoweidlem31  37930  stoweidlem59  37958  stirlinglem13  37986  fourierdlem41  38049  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem48  38056  fourierdlem51  38059  fourierdlem53  38061  fourierdlem70  38078  fourierdlem71  38079  fourierdlem73  38081  fourierdlem80  38088  fourierdlem81  38089  fourierdlem89  38097  fourierdlem91  38099  fourierdlem93  38101  fourierdlem97  38105  elaa2  38137  qndenserrnopnlem  38204  salexct  38231  sge0tsms  38260  sge0f1o  38262  sge0fsum  38267  sge0supre  38269  sge0sup  38271  sge0rnbnd  38273  sge0gerp  38275  sge0pnffigt  38276  sge0lefi  38278  sge0ltfirp  38280  sge0resrn  38284  sge0resplit  38286  sge0split  38289  sge0iunmptlemfi  38293  sge0iunmptlemre  38295  sge0iunmpt  38298  sge0rpcpnf  38301  sge0isum  38307  sge0xp  38309  sge0xaddlem2  38314  sge0uzfsumgt  38324  nnfoctbdjlem  38331  nnfoctbdj  38332  iundjiun  38336  meadjiunlem  38341  carageniuncllem1  38380  carageniuncllem2  38381  caratheodorylem1  38385  caratheodorylem2  38386  isomenndlem  38389  ovnsupge0  38417  ovnlerp  38422  ovncvrrp  38424  ovnsubaddlem1  38430  hoidmvval0  38447  hoidmv1lelem3  38453  hoidmv1le  38454  hoidmvlelem1  38455  hoidmvlelem2  38456  hoidmvlelem3  38457  ovnhoilem2  38462  opnvonmbllem2  38493  iccpartiltu  38774  fundmge2nop  39068  uhgrauhgrbi  39209  ausgrumgri  39302  ausgrusgri  39303  usgrausgrb  39304  usgredg2vtxeuALT  39349  ushgredgedga  39356  ushgredgedgaloop  39358  nbuhgr2vtx1edgb  39470  cusgrsize2inds  39564  upgrewlkle2  39673  red1wlk  39717  pthdivtx  39762  pthdadjvtx  39763  upgr2pthnlp  39765  upgrspths1wlk  39770  cyclnsPth  39822  1pthon2v-av  39868  uhgr3cyclex  39923  uhgrauhgbi  39959  rngccatidALTV  40264  ringccatidALTV  40327  nzerooringczr  40347  lcosslsp  40504  fllog2  40652  dignn0flhalf  40702