Theorem syl3an2 1360

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

Ref	Expression
syl3an2.1	|- ( ph -> ch )
syl3an2.2	|- ( ( ps /\ ch /\ th ) -> ta )

Assertion

Ref	Expression
syl3an2	|- ( ( ps /\ ph /\ th ) -> ta )

Proof of Theorem syl3an2

Step	Hyp	Ref	Expression
1		syl3an2.1	. . 3 |- ( ph -> ch )
2		syl3an2.2	. . . 4 |- ( ( ps /\ ch /\ th ) -> ta )
3	2	3exp 1264	. . 3 |- ( ps -> ( ch -> ( th -> ta ) ) )
4	1, 3	syl5 34	. 2 |- ( ps -> ( ph -> ( th -> ta ) ) )
5	4	3imp 1256	1 |- ( ( ps /\ ph /\ th ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  syl3an2b  1363  syl3an2br  1366  syl3anl2  1375  odi  7659  omass  7660  nndi  7703  nnmass  7704  omabslem  7726  winainf  9516  divsubdir  10721  divdiv32  10733  ltdiv2  10909  peano2uz  11741  irrmul  11813  supxrunb1  12149  fzoshftral  12585  ltdifltdiv  12635  axdc4uzlem  12782  expdiv  12911  bcval5  13105  ccats1val1  13403  rediv  13871  imdiv  13878  absdiflt  14057  absdifle  14058  iseraltlem3  14414  retancl  14872  tanneg  14878  lcmgcdeq  15325  prmdvdsexpb  15428  dvdsprmpweqnn  15589  mulgaddcomlem  17563  mulginvcom  17565  pmtrfb  17885  lspssp  18988  mdetunilem7  20424  m2detleiblem3  20435  m2detleiblem4  20436  pmatcollpw  20586  pmatcollpwscmat  20596  chpmatply1  20637  chfacfscmulgsum  20665  chfacfpmmulcl  20666  chfacfpmmul0  20667  chfacfpmmulgsum  20669  chfacfpmmulgsum2  20670  cayhamlem1  20671  cpmadurid  20672  cpmadugsumlemC  20680  cpmadugsumlemF  20681  cpmadugsumfi  20682  cpmidgsum2  20684  islp2  20949  fmfg  21753  fmufil  21763  flffbas  21799  lmflf  21809  uffcfflf  21843  blres  22236  ncvsge0  22953  caucfil  23081  cmetcusp1  23149  deg1mul3  23875  quotval  24047  cusgr3vnbpr  26332  clwwlkinwwlk  26905  nvsge0  27519  hvsubass  27901  hvsubdistr2  27907  hvsubcan  27931  his2sub  27949  chlub  28368  spanunsni  28438  homco1  28660  homulass  28661  cnlnadjlem2  28927  adjmul  28951  chirredlem2  29250  atmd2  29259  mdsymlem5  29266  climuzcnv  31565  f1ocan2fv  33522  isdrngo2  33757  atncvrN  34602  cvlatcvr1  34628  eluzrabdioph  37370  iocmbl  37798  rp-isfinite6  37864  dvconstbi  38533  eelT11  38932  eelT12  38934  eelTT1  38935  eel0T1  38937  nn0digval  42394  dignn0flhalf  42412  sinhpcosh  42481  reseccl  42494  recsccl  42495  recotcl  42496  onetansqsecsq  42502