Theorem syld3an3 1261

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 981	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2		simp2 982	. 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 1216	1 |- ( ( ph /\ ps /\ ch ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 962

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 964

This theorem is referenced by:  syld3an1  1262  syld3an2  1263  brelrng  4770  moriotass  5758  nnncan1  7998  lediv1  8627  modqval  10097  modqvalr  10098  modqcl  10099  flqpmodeq  10100  modq0  10102  modqge0  10105  modqlt  10106  modqdiffl  10108  modqdifz  10109  modqvalp1  10116  exp3val  10295  bcval4  10498  dvdsmultr1  11531  dvdssub2  11535  divalglemeuneg  11620  ndvdsadd  11628  basgen2  12250  opnneiss  12327  cnpf2  12376  sincosq1lem  12906