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  4893  moriotass  5902  nnncan1  8255  lediv1  8888  modqval  10395  modqvalr  10396  modqcl  10397  flqpmodeq  10398  modq0  10400  modqge0  10403  modqlt  10404  modqdiffl  10406  modqdifz  10407  modqvalp1  10414  exp3val  10612  bcval4  10823  dvdsmultr1  11974  dvdssub2  11978  divalglemeuneg  12064  ndvdsadd  12072  grpsubf  13151  grpinvsub  13154  grpnpcan  13164  mulginvcom  13217  mulginvinv  13218  subgsubcl  13255  qussub  13307  ghmsub  13321  dvrcl  13631  unitdvcl  13632  basgen2  14249  opnneiss  14326  cnpf2  14375  sincosq1lem  14960