Theorem syld3an3 1295

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  syld3an1  1296  syld3an2  1297  brelrng  4910  moriotass  5930  nnncan1  8310  lediv1  8944  modqval  10471  modqvalr  10472  modqcl  10473  flqpmodeq  10474  modq0  10476  modqge0  10479  modqlt  10480  modqdiffl  10482  modqdifz  10483  modqvalp1  10490  exp3val  10688  bcval4  10899  ccatval3  11058  ccatfv0  11062  ccatval1lsw  11063  ccatval21sw  11064  lswccatn0lsw  11070  pfxsuff1eqwrdeq  11153  dvdsmultr1  12175  dvdssub2  12179  divalglemeuneg  12267  ndvdsadd  12275  grpsubf  13444  grpinvsub  13447  grpnpcan  13457  mulginvcom  13516  mulginvinv  13517  subgsubcl  13554  qussub  13606  ghmsub  13620  dvrcl  13930  unitdvcl  13931  basgen2  14586  opnneiss  14663  cnpf2  14712  sincosq1lem  15330