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  4928  moriotass  5951  nnncan1  8343  lediv1  8977  modqval  10506  modqvalr  10507  modqcl  10508  flqpmodeq  10509  modq0  10511  modqge0  10514  modqlt  10515  modqdiffl  10517  modqdifz  10518  modqvalp1  10525  exp3val  10723  bcval4  10934  ccatval3  11093  ccatfv0  11097  ccatval1lsw  11098  ccatval21sw  11099  lswccatn0lsw  11105  pfxsuff1eqwrdeq  11190  pfxccatid  11232  dvdsmultr1  12257  dvdssub2  12261  divalglemeuneg  12349  ndvdsadd  12357  grpsubf  13526  grpinvsub  13529  grpnpcan  13539  mulginvcom  13598  mulginvinv  13599  subgsubcl  13636  qussub  13688  ghmsub  13702  dvrcl  14012  unitdvcl  14013  basgen2  14668  opnneiss  14745  cnpf2  14794  sincosq1lem  15412