Theorem syld3an2 1311

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

Syntax hints:   -> wi 4   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  nppcan2  9904  nnncan  9908  nnncan2  9910  ltdivmul  10479  ledivmul  10480  ltdiv23  10497  lediv23  10498  xrmaxlt  11476  xrltmin  11477  xrmaxle  11478  xrlemin  11479  swrdtrcfv  12782  dvdssub2  14320  dvdsgcdb  14483  lcmdvdsb  14543  vdwapun  14878  poslubdg  16337  ipodrsfi  16351  matinvgcell  19382  mdetrsca2  19551  mdetrlin2  19554  mdetunilem5  19563  decpmatmul  19718  islp3  20084  bddibl  22665  gxinv  25834  gxinv2  25835  vcnegsubdi2  26030  nvpi  26131  nvabs  26138  nmmulg  28602  ghomgsg  30090  subdivcomb2  30139  lineid  30626  oplecon1b  32466  opltcon1b  32470  oldmm2  32483  oldmj2  32487  cmt3N  32516  2llnneN  32673  cvrexchlem  32683  pmod2iN  33113  polcon2N  33183  paddatclN  33213  osumcllem3N  33222  ltrnval1  33398  cdleme48fv  33765  cdlemg33b  33973  trlcolem  33992  cdlemh  34083  cdlemi1  34084  cdlemi2  34085  cdlemi  34086  cdlemk4  34100  cdlemk19u1  34235  cdlemn3  34464  hgmapfval  35156  pell14qrgap  35419  stoweidlem22  37441  stoweidlem26  37445  sigarexp  37858  pfxtrcfv  38322  pfxco  38359  lindszr  39012