Theorem syld3an3 1294

Description: A syllogism inference. (Contributed by NM, 20-May-2007.)

Hypotheses

Ref	Expression
syld3an3.1	|- ( ( ph /\ ps /\ ch ) -> th )
syld3an3.2	|- ( ( ph /\ ps /\ th ) -> ta )

Assertion

Ref	Expression
syld3an3	|- ( ( ph /\ ps /\ ch ) -> ta )

Proof of Theorem syld3an3

Step	Hyp	Ref	Expression
1		simp1 999	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2		simp2 1000	. 2 |- ( ( ph /\ ps /\ ch ) -> ps )
3		syld3an3.1	. 2 |- ( ( ph /\ ps /\ ch ) -> th )
4		syld3an3.2	. 2 |- ( ( ph /\ ps /\ th ) -> ta )
5	1, 2, 3, 4	syl3anc 1249	1 |- ( ( ph /\ ps /\ ch ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  syld3an1  1295  syld3an2  1296  brelrng  4898  moriotass  5909  nnncan1  8279  lediv1  8913  modqval  10433  modqvalr  10434  modqcl  10435  flqpmodeq  10436  modq0  10438  modqge0  10441  modqlt  10442  modqdiffl  10444  modqdifz  10445  modqvalp1  10452  exp3val  10650  bcval4  10861  dvdsmultr1  12013  dvdssub2  12017  divalglemeuneg  12105  ndvdsadd  12113  grpsubf  13281  grpinvsub  13284  grpnpcan  13294  mulginvcom  13353  mulginvinv  13354  subgsubcl  13391  qussub  13443  ghmsub  13457  dvrcl  13767  unitdvcl  13768  basgen2  14401  opnneiss  14478  cnpf2  14527  sincosq1lem  15145