Theorem syl3an2 1301

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

Syntax hints:   -> wi 4   /\ w3a 984

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 189  df-an 373  df-3an 986

This theorem is referenced by:  syl3an2b  1304  syl3an2br  1307  syl3anl2  1316  odi  7277  omass  7278  nndi  7321  nnmass  7322  omabslem  7344  winainf  9116  divsubdir  10300  divdiv32  10312  ltdiv2  10489  peano2uz  11209  irrmul  11286  supxrunb1  11602  fzoshftral  12019  ltdifltdiv  12063  axdc4uzlem  12192  expdiv  12320  bcval5  12500  ccats1val1  12754  rediv  13187  imdiv  13194  absdiflt  13373  absdifle  13374  iseraltlem3  13743  retancl  14189  tanneg  14195  lcmgcdeq  14570  prmdvdsexpb  14661  pmtrfb  17099  lspssp  18204  mdetunilem7  19636  m2detleiblem3  19647  m2detleiblem4  19648  pmatcollpw  19798  pmatcollpwscmat  19808  chpmatply1  19849  chfacfscmulgsum  19877  chfacfpmmulcl  19878  chfacfpmmul0  19879  chfacfpmmulgsum  19881  chfacfpmmulgsum2  19882  cayhamlem1  19883  cpmadurid  19884  cpmadugsumlemC  19892  cpmadugsumlemF  19893  cpmadugsumfi  19894  cpmidgsum2  19896  islp2  20154  fmfg  20957  fmufil  20967  flffbas  21003  lmflf  21013  uffcfflf  21047  blres  21439  caucfil  22246  cmetcusp1  22313  deg1mul3  23057  quotval  23238  cusgra3vnbpr  25186  gxid  25994  nvsge0  26285  hvsubass  26690  hvsubdistr2  26696  hvsubcan  26720  his2sub  26738  chlub  27155  spanunsni  27225  homco1  27447  homulass  27448  cnlnadjlem2  27714  adjmul  27738  chirredlem2  28037  atmd2  28046  mdsymlem5  28053  climuzcnv  30308  f1ocan2fv  32047  isdrngo2  32190  atncvrN  32875  cvlatcvr1  32901  eluzrabdioph  35643  iocmbl  36091  rp-isfinite6  36157  dvconstbi  36677  eelT11  37083  eelT12  37087  eelTT1  37088  eel0T1  37090  cusgr3vnbpr  39486  nn0digval  40398  dignn0flhalf  40416  sinhpcosh  40447  reseccl  40460  recsccl  40461  recotcl  40462  onetansqsecsq  40468