Theorem syl3an2 1253

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 1187	. . 3 |- ( ps -> ( ch -> ( th -> ta ) ) )
4	1, 3	syl5 32	. 2 |- ( ps -> ( ph -> ( th -> ta ) ) )
5	4	3imp 1182	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  1256  syl3an2br  1259  syl3anl2  1268  odi  7120  omass  7121  nndi  7164  nnmass  7165  omabslem  7187  winainf  8964  divsubdir  10130  divdiv32  10142  ltdiv2  10320  peano2uz  11011  irrmul  11081  supxrunb1  11385  fzoshftral  11739  ltdifltdiv  11781  axdc4uzlem  11907  expdiv  12017  bcval5  12197  ccats1val1  12410  cats1un  12474  rediv  12724  imdiv  12731  absdiflt  12909  absdifle  12910  iseraltlem3  13265  retancl  13530  tanneg  13536  prmdvdsexpb  13905  pmtrfb  16075  lspssp  17177  mdetunilem7  18542  m2detleiblem3  18553  m2detleiblem4  18554  islp2  18867  fmfg  19640  fmufil  19650  flffbas  19686  lmflf  19696  uffcfflf  19730  blres  20124  caucfil  20912  cmetcusp1OLD  20981  cmetcusp1  20982  deg1mul3  21705  quotval  21876  cusgra3vnbpr  23510  gxid  23897  nvsge0  24188  hvsubass  24583  hvsubdistr2  24589  hvsubcan  24613  his2sub  24631  chlub  25049  spanunsni  25119  homco1  25342  homulass  25343  cnlnadjlem2  25609  adjmul  25633  chirredlem2  25932  atmd2  25941  mdsymlem5  25948  climuzcnv  27452  f1ocan2fv  28761  isdrngo2  28904  eluzrabdioph  29284  iocmbl  29728  dvconstbi  29748  pmatcollpw3  31240  pmatcollpw3fi  31241  pmatcollpwscmat  31250  cpmatply1  31287  chfacfscmulgsum  31316  chfacfpmmulcl  31317  chfacfpmmul0  31318  chfacfpmmulgsum  31320  chfacfpmmulgsum2  31321  cayhamlem1  31322  cpmadurid  31323  cpmadugsumlemC  31331  cpmadugsumlemF  31332  cpmadugsumfi  31333  cpmidgsum2  31335  sinhpcosh  31373  reseccl  31386  recsccl  31387  recotcl  31388  onetansqsecsq  31394  eelT11  31734  eelT12  31738  eelTT1  31740  eel0T1  31742  atncvrN  33268  cvlatcvr1  33294