Theorem syld3an2 1260

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 1188	. . 3 |- ( ( ph /\ th /\ ch ) -> ps )
3		syld3an2.2	. . . 4 |- ( ( ph /\ ps /\ th ) -> ta )
4	3	3com23 1188	. . 3 |- ( ( ph /\ th /\ ps ) -> ta )
5	2, 4	syld3an3 1258	. 2 |- ( ( ph /\ th /\ ch ) -> ta )
6	5	3com23 1188	1 |- ( ( ph /\ ch /\ th ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 960

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 962

This theorem is referenced by:  nppcan2  9636  nnncan  9640  nnncan2  9642  ltdivmul  10200  ledivmul  10201  ltdiv23  10219  lediv23  10220  xrmaxlt  11149  xrltmin  11150  xrmaxle  11151  xrlemin  11152  swrdtrcfv  12333  dvdssub2  13566  dvdsgcdb  13724  vdwapun  14031  poslubdg  15315  ipodrsfi  15329  mdetrsca2  18370  mdetrlin2  18372  mdetunilem5  18381  islp3  18709  bddibl  21276  gxinv  23692  gxinv2  23693  vcnegsubdi2  23888  nvpi  23989  nvabs  23996  nmmulg  26333  ghomgsg  27241  subdivcomb2  27314  lineid  28043  pell14qrgap  29141  stoweidlem22  29742  stoweidlem26  29746  sigarexp  29820  lindszr  30844  oplecon1b  32568  opltcon1b  32572  oldmm2  32585  oldmj2  32589  cmt3N  32618  2llnneN  32775  cvrexchlem  32785  pmod2iN  33215  polcon2N  33285  paddatclN  33315  osumcllem3N  33324  ltrnval1  33500  cdleme48fv  33865  cdlemg33b  34073  trlcolem  34092  cdlemh  34183  cdlemi1  34184  cdlemi2  34185  cdlemi  34186  cdlemk4  34200  cdlemk19u1  34335  cdlemn3  34564  hgmapfval  35256