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  4765  moriotass  5751  nnncan1  7991  lediv1  8620  modqval  10090  modqvalr  10091  modqcl  10092  flqpmodeq  10093  modq0  10095  modqge0  10098  modqlt  10099  modqdiffl  10101  modqdifz  10102  modqvalp1  10109  exp3val  10288  bcval4  10491  dvdsmultr1  11520  dvdssub2  11524  divalglemeuneg  11609  ndvdsadd  11617  basgen2  12239  opnneiss  12316  cnpf2  12365  sincosq1lem  12895