Theorem syld3an3 1265

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

Syntax hints:   -> wi 4   /\ w3a 963

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 965

This theorem is referenced by:  syld3an1  1266  syld3an2  1267  brelrng  4814  moriotass  5802  nnncan1  8094  lediv1  8723  modqval  10205  modqvalr  10206  modqcl  10207  flqpmodeq  10208  modq0  10210  modqge0  10213  modqlt  10214  modqdiffl  10216  modqdifz  10217  modqvalp1  10224  exp3val  10403  bcval4  10608  dvdsmultr1  11706  dvdssub2  11710  divalglemeuneg  11795  ndvdsadd  11803  basgen2  12441  opnneiss  12518  cnpf2  12567  sincosq1lem  13106