Theorem syld3an2 1273

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

Syntax hints:   -> wi 4   /\ w3a 971

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 369  df-3an 973

This theorem is referenced by:  nppcan2  9763  nnncan  9767  nnncan2  9769  ltdivmul  10334  ledivmul  10335  ltdiv23  10352  lediv23  10353  xrmaxlt  11303  xrltmin  11304  xrmaxle  11305  xrlemin  11306  swrdtrcfv  12577  dvdssub2  14025  dvdsgcdb  14184  vdwapun  14494  poslubdg  15896  ipodrsfi  15910  matinvgcell  19022  mdetrsca2  19191  mdetrlin2  19194  mdetunilem5  19203  decpmatmul  19358  islp3  19733  bddibl  22331  gxinv  25389  gxinv2  25390  vcnegsubdi2  25585  nvpi  25686  nvabs  25693  nmmulg  28102  ghomgsg  29222  subdivcomb2  29272  lineid  29886  pell14qrgap  30976  lcmdvdsb  31385  stoweidlem22  31970  stoweidlem26  31974  sigarexp  32242  pfxtrcfv  32576  pfxco  32613  lindszr  33270  oplecon1b  35339  opltcon1b  35343  oldmm2  35356  oldmj2  35360  cmt3N  35389  2llnneN  35546  cvrexchlem  35556  pmod2iN  35986  polcon2N  36056  paddatclN  36086  osumcllem3N  36095  ltrnval1  36271  cdleme48fv  36638  cdlemg33b  36846  trlcolem  36865  cdlemh  36956  cdlemi1  36957  cdlemi2  36958  cdlemi  36959  cdlemk4  36973  cdlemk19u1  37108  cdlemn3  37337  hgmapfval  38029