Theorem syld3an3 1214

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 938	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2		simp2 939	. 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 1169	1 |- ( ( ph /\ ps /\ ch ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  syld3an1  1215  syld3an2  1216  brelrng  4583  moriotass  5516  nnncan1  7344  lediv1  7947  modqval  9326  modqvalr  9327  modqcl  9328  flqpmodeq  9329  modq0  9331  modqge0  9334  modqlt  9335  modqdiffl  9337  modqdifz  9338  modqvalp1  9345  expival  9478  bcval4  9679  dvdsmultr1  10233  dvdssub2  10237  divalglemeuneg  10323  ndvdsadd  10331