Theorem syl3an2 1262

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 1195	. . 3 |- ( ps -> ( ch -> ( th -> ta ) ) )
4	1, 3	syl5 32	. 2 |- ( ps -> ( ph -> ( th -> ta ) ) )
5	4	3imp 1190	1 |- ( ( ps /\ ph /\ th ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 973

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 371  df-3an 975

This theorem is referenced by:  syl3an2b  1265  syl3an2br  1268  syl3anl2  1277  odi  7225  omass  7226  nndi  7269  nnmass  7270  omabslem  7292  winainf  9068  divsubdir  10236  divdiv32  10248  ltdiv2  10426  peano2uz  11130  irrmul  11203  supxrunb1  11507  fzoshftral  11887  ltdifltdiv  11930  axdc4uzlem  12056  expdiv  12180  bcval5  12360  ccats1val1  12589  cats1un  12660  rediv  12923  imdiv  12930  absdiflt  13109  absdifle  13110  iseraltlem3  13465  retancl  13734  tanneg  13740  prmdvdsexpb  14111  pmtrfb  16286  lspssp  17417  mdetunilem7  18887  m2detleiblem3  18898  m2detleiblem4  18899  pmatcollpw  19049  pmatcollpwscmat  19059  chpmatply1  19100  chfacfscmulgsum  19128  chfacfpmmulcl  19129  chfacfpmmul0  19130  chfacfpmmulgsum  19132  chfacfpmmulgsum2  19133  cayhamlem1  19134  cpmadurid  19135  cpmadugsumlemC  19143  cpmadugsumlemF  19144  cpmadugsumfi  19145  cpmidgsum2  19147  islp2  19412  fmfg  20185  fmufil  20195  flffbas  20231  lmflf  20241  uffcfflf  20275  blres  20669  caucfil  21457  cmetcusp1OLD  21526  cmetcusp1  21527  deg1mul3  22251  quotval  22422  cusgra3vnbpr  24141  gxid  24951  nvsge0  25242  hvsubass  25637  hvsubdistr2  25643  hvsubcan  25667  his2sub  25685  chlub  26103  spanunsni  26173  homco1  26396  homulass  26397  cnlnadjlem2  26663  adjmul  26687  chirredlem2  26986  atmd2  26995  mdsymlem5  27002  climuzcnv  28512  f1ocan2fv  29821  isdrngo2  29964  eluzrabdioph  30343  iocmbl  30785  lcmgcdeq  30816  dvconstbi  30839  sinhpcosh  32215  reseccl  32228  recsccl  32229  recotcl  32230  onetansqsecsq  32236  eelT11  32576  eelT12  32580  eelTT1  32582  eel0T1  32584  atncvrN  34112  cvlatcvr1  34138