Theorem syld3an3 1273

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 987	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2		simp2 988	. 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 1228	1 |- ( ( ph /\ ps /\ ch ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 968

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 970

This theorem is referenced by:  syld3an1  1274  syld3an2  1275  brelrng  4835  moriotass  5826  nnncan1  8134  lediv1  8764  modqval  10259  modqvalr  10260  modqcl  10261  flqpmodeq  10262  modq0  10264  modqge0  10267  modqlt  10268  modqdiffl  10270  modqdifz  10271  modqvalp1  10278  exp3val  10457  bcval4  10665  dvdsmultr1  11771  dvdssub2  11775  divalglemeuneg  11860  ndvdsadd  11868  basgen2  12721  opnneiss  12798  cnpf2  12847  sincosq1lem  13386