Theorem syld3an3 1283

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 997	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2		simp2 998	. 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 1238	1 |- ( ( ph /\ ps /\ ch ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  syld3an1  1284  syld3an2  1285  brelrng  4860  moriotass  5861  nnncan1  8195  lediv1  8828  modqval  10326  modqvalr  10327  modqcl  10328  flqpmodeq  10329  modq0  10331  modqge0  10334  modqlt  10335  modqdiffl  10337  modqdifz  10338  modqvalp1  10345  exp3val  10524  bcval4  10734  dvdsmultr1  11840  dvdssub2  11844  divalglemeuneg  11930  ndvdsadd  11938  grpsubf  12954  grpinvsub  12957  grpnpcan  12967  mulginvcom  13013  mulginvinv  13014  subgsubcl  13050  dvrcl  13309  unitdvcl  13310  basgen2  13666  opnneiss  13743  cnpf2  13792  sincosq1lem  14331