Theorem syl3an2 1252

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

Syntax hints:   -> wi 4   /\ w3a 965

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 967

This theorem is referenced by:  syl3an2b  1255  syl3an2br  1258  syl3anl2  1267  odi  7010  omass  7011  nndi  7054  nnmass  7055  omabslem  7077  winainf  8853  divsubdir  10019  divdiv32  10031  ltdiv2  10209  peano2uz  10900  irrmul  10970  supxrunb1  11274  fzoshftral  11628  ltdifltdiv  11670  axdc4uzlem  11796  expdiv  11906  bcval5  12086  ccats1val1  12298  cats1un  12362  rediv  12612  imdiv  12619  absdiflt  12797  absdifle  12798  iseraltlem3  13153  retancl  13418  tanneg  13424  prmdvdsexpb  13793  pmtrfb  15962  lspssp  17046  mdetunilem7  18399  m2detleiblem3  18410  m2detleiblem4  18411  islp2  18724  fmfg  19497  fmufil  19507  flffbas  19543  lmflf  19553  uffcfflf  19587  blres  19981  caucfil  20769  cmetcusp1OLD  20838  cmetcusp1  20839  deg1mul3  21562  quotval  21733  cusgra3vnbpr  23324  gxid  23711  nvsge0  24002  hvsubass  24397  hvsubdistr2  24403  hvsubcan  24427  his2sub  24445  chlub  24863  spanunsni  24933  homco1  25156  homulass  25157  cnlnadjlem2  25423  adjmul  25447  chirredlem2  25746  atmd2  25755  mdsymlem5  25762  climuzcnv  27267  f1ocan2fv  28574  isdrngo2  28717  eluzrabdioph  29097  iocmbl  29541  dvconstbi  29561  pmatcollpw2  30821  sinhpcosh  30964  reseccl  30977  recsccl  30978  recotcl  30979  onetansqsecsq  30985  eelT11  31319  eelT12  31323  eelTT1  31325  eel0T1  31327  atncvrN  32800  cvlatcvr1  32826