Theorem syld3an3 1278

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 992	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2		simp2 993	. 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 1233	1 |- ( ( ph /\ ps /\ ch ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 973

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

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  syld3an1  1279  syld3an2  1280  brelrng  4842  moriotass  5837  nnncan1  8155  lediv1  8785  modqval  10280  modqvalr  10281  modqcl  10282  flqpmodeq  10283  modq0  10285  modqge0  10288  modqlt  10289  modqdiffl  10291  modqdifz  10292  modqvalp1  10299  exp3val  10478  bcval4  10686  dvdsmultr1  11793  dvdssub2  11797  divalglemeuneg  11882  ndvdsadd  11890  basgen2  12875  opnneiss  12952  cnpf2  13001  sincosq1lem  13540