Theorem syld3an2 1266

Description: A syllogism inference. (Contributed by NM, 20-May-2007.)

Hypotheses

Ref	Expression
syld3an2.1	|- ( ( ph /\ ch /\ th ) -> ps )
syld3an2.2	|- ( ( ph /\ ps /\ th ) -> ta )

Assertion

Ref	Expression
syld3an2	|- ( ( ph /\ ch /\ th ) -> ta )

Proof of Theorem syld3an2

Step	Hyp	Ref	Expression
1		syld3an2.1	. . . 4 |- ( ( ph /\ ch /\ th ) -> ps )
2	1	3com23 1194	. . 3 |- ( ( ph /\ th /\ ch ) -> ps )
3		syld3an2.2	. . . 4 |- ( ( ph /\ ps /\ th ) -> ta )
4	3	3com23 1194	. . 3 |- ( ( ph /\ th /\ ps ) -> ta )
5	2, 4	syld3an3 1264	. 2 |- ( ( ph /\ th /\ ch ) -> ta )
6	5	3com23 1194	1 |- ( ( ph /\ ch /\ 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:  nppcan2  9746  nnncan  9750  nnncan2  9752  ltdivmul  10310  ledivmul  10311  ltdiv23  10329  lediv23  10330  xrmaxlt  11259  xrltmin  11260  xrmaxle  11261  xrlemin  11262  swrdtrcfv  12450  dvdssub2  13683  dvdsgcdb  13841  vdwapun  14148  poslubdg  15433  ipodrsfi  15447  mdetrsca2  18537  mdetrlin2  18540  mdetunilem5  18549  islp3  18877  bddibl  21445  gxinv  23904  gxinv2  23905  vcnegsubdi2  24100  nvpi  24201  nvabs  24208  nmmulg  26537  ghomgsg  27451  subdivcomb2  27524  lineid  28253  pell14qrgap  29359  stoweidlem22  29960  stoweidlem26  29964  sigarexp  30038  matinvgcell  31014  lindszr  31117  decpmatmul  31241  oplecon1b  33165  opltcon1b  33169  oldmm2  33182  oldmj2  33186  cmt3N  33215  2llnneN  33372  cvrexchlem  33382  pmod2iN  33812  polcon2N  33882  paddatclN  33912  osumcllem3N  33921  ltrnval1  34097  cdleme48fv  34462  cdlemg33b  34670  trlcolem  34689  cdlemh  34780  cdlemi1  34781  cdlemi2  34782  cdlemi  34783  cdlemk4  34797  cdlemk19u1  34932  cdlemn3  35161  hgmapfval  35853