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  4858  moriotass  5858  nnncan1  8192  lediv1  8825  modqval  10323  modqvalr  10324  modqcl  10325  flqpmodeq  10326  modq0  10328  modqge0  10331  modqlt  10332  modqdiffl  10334  modqdifz  10335  modqvalp1  10342  exp3val  10521  bcval4  10731  dvdsmultr1  11837  dvdssub2  11841  divalglemeuneg  11927  ndvdsadd  11935  grpsubf  12948  grpinvsub  12951  grpnpcan  12961  mulginvcom  13006  mulginvinv  13007  subgsubcl  13043  dvrcl  13302  unitdvcl  13303  basgen2  13517  opnneiss  13594  cnpf2  13643  sincosq1lem  14182