Theorem syl3an2 1298

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

Syntax hints:   -> wi 4   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  syl3an2b  1301  syl3an2br  1304  syl3anl2  1313  odi  7279  omass  7280  nndi  7323  nnmass  7324  omabslem  7346  winainf  9108  divsubdir  10292  divdiv32  10304  ltdiv2  10481  peano2uz  11201  irrmul  11278  supxrunb1  11594  fzoshftral  12008  ltdifltdiv  12052  axdc4uzlem  12181  expdiv  12309  bcval5  12489  ccats1val1  12733  rediv  13162  imdiv  13169  absdiflt  13348  absdifle  13349  iseraltlem3  13717  retancl  14163  tanneg  14169  lcmgcdeq  14537  prmdvdsexpb  14628  pmtrfb  17058  lspssp  18152  mdetunilem7  19580  m2detleiblem3  19591  m2detleiblem4  19592  pmatcollpw  19742  pmatcollpwscmat  19752  chpmatply1  19793  chfacfscmulgsum  19821  chfacfpmmulcl  19822  chfacfpmmul0  19823  chfacfpmmulgsum  19825  chfacfpmmulgsum2  19826  cayhamlem1  19827  cpmadurid  19828  cpmadugsumlemC  19836  cpmadugsumlemF  19837  cpmadugsumfi  19838  cpmidgsum2  19840  islp2  20098  fmfg  20901  fmufil  20911  flffbas  20947  lmflf  20957  uffcfflf  20991  blres  21383  caucfil  22172  cmetcusp1  22239  deg1mul3  22971  quotval  23152  cusgra3vnbpr  25079  gxid  25887  nvsge0  26178  hvsubass  26573  hvsubdistr2  26579  hvsubcan  26603  his2sub  26621  chlub  27038  spanunsni  27108  homco1  27330  homulass  27331  cnlnadjlem2  27597  adjmul  27621  chirredlem2  27920  atmd2  27929  mdsymlem5  27936  climuzcnv  30144  f1ocan2fv  31802  isdrngo2  31945  atncvrN  32634  cvlatcvr1  32660  eluzrabdioph  35402  iocmbl  35844  rp-isfinite6  35910  dvconstbi  36368  eelT11  36775  eelT12  36779  eelTT1  36781  eel0T1  36783  nn0digval  39229  dignn0flhalf  39247  sinhpcosh  39278  reseccl  39291  recsccl  39292  recotcl  39293  onetansqsecsq  39299