Theorem syld3an2 1231

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

Syntax hints:   -> wi 4   /\ w3a 936

This theorem is referenced by:  nppcan2  9288  nnncan  9292  nnncan2  9294  ltdivmul  9838  ledivmul  9839  ltdiv23  9857  lediv23  9858  xrmaxlt  10725  xrltmin  10726  xrmaxle  10727  xrlemin  10728  dvdssub2  12842  dvdsgcdb  12999  vdwapun  13297  poslubdg  14530  ipodrsfi  14544  bddibl  19684  gxinv  21811  gxinv2  21812  vcnegsubdi2  22007  nvpi  22108  nvabs  22115  nmmulg  24305  ghomgsg  25057  subdivcomb2  25149  lineid  25921  pell14qrgap  26828  stoweidlem22  27638  stoweidlem26  27642  sigarexp  27716  oplecon1b  29684  opltcon1b  29688  oldmm2  29701  oldmj2  29705  cmt3N  29734  2llnneN  29891  cvrexchlem  29901  pmod2iN  30331  polcon2N  30401  paddatclN  30431  osumcllem3N  30440  ltrnval1  30616  cdleme48fv  30981  cdlemg33b  31189  trlcolem  31208  cdlemh  31299  cdlemi1  31300  cdlemi2  31301  cdlemi  31302  cdlemk4  31316  cdlemk19u1  31451  cdlemn3  31680  hgmapfval  32372

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938