Theorem syld3an2 1275

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

Syntax hints:   -> wi 4   /\ w3a 973

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 975

This theorem is referenced by:  nppcan2  9846  nnncan  9850  nnncan2  9852  ltdivmul  10413  ledivmul  10414  ltdiv23  10432  lediv23  10433  xrmaxlt  11378  xrltmin  11379  xrmaxle  11380  xrlemin  11381  swrdtrcfv  12625  dvdssub2  13875  dvdsgcdb  14034  vdwapun  14344  poslubdg  15629  ipodrsfi  15643  matinvgcell  18701  mdetrsca2  18870  mdetrlin2  18873  mdetunilem5  18882  decpmatmul  19037  islp3  19410  bddibl  21978  gxinv  24945  gxinv2  24946  vcnegsubdi2  25141  nvpi  25242  nvabs  25249  nmmulg  27582  ghomgsg  28505  subdivcomb2  28578  lineid  29307  pell14qrgap  30413  lcmdvdsb  30817  stoweidlem22  31322  stoweidlem26  31326  sigarexp  31543  lindszr  32143  oplecon1b  33998  opltcon1b  34002  oldmm2  34015  oldmj2  34019  cmt3N  34048  2llnneN  34205  cvrexchlem  34215  pmod2iN  34645  polcon2N  34715  paddatclN  34745  osumcllem3N  34754  ltrnval1  34930  cdleme48fv  35295  cdlemg33b  35503  trlcolem  35522  cdlemh  35613  cdlemi1  35614  cdlemi2  35615  cdlemi  35616  cdlemk4  35630  cdlemk19u1  35765  cdlemn3  35994  hgmapfval  36686