Theorem syld3an3 1294

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 999	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2		simp2 1000	. 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 1249	1 |- ( ( ph /\ ps /\ ch ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  syld3an1  1295  syld3an2  1296  brelrng  4894  moriotass  5903  nnncan1  8257  lediv1  8890  modqval  10398  modqvalr  10399  modqcl  10400  flqpmodeq  10401  modq0  10403  modqge0  10406  modqlt  10407  modqdiffl  10409  modqdifz  10410  modqvalp1  10417  exp3val  10615  bcval4  10826  dvdsmultr1  11977  dvdssub2  11981  divalglemeuneg  12067  ndvdsadd  12075  grpsubf  13154  grpinvsub  13157  grpnpcan  13167  mulginvcom  13220  mulginvinv  13221  subgsubcl  13258  qussub  13310  ghmsub  13324  dvrcl  13634  unitdvcl  13635  basgen2  14260  opnneiss  14337  cnpf2  14386  sincosq1lem  15001