Theorem syld3an3 1319

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 1024	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2		simp2 1025	. 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 1274	1 |- ( ( ph /\ ps /\ ch ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  syld3an1  1320  syld3an2  1321  brelrng  4988  moriotass  6034  nnncan1  8509  lediv1  9143  modqval  10686  modqvalr  10687  modqcl  10688  flqpmodeq  10689  modq0  10691  modqge0  10694  modqlt  10695  modqdiffl  10697  modqdifz  10698  modqvalp1  10705  exp3val  10903  bcval4  11114  ccatval3  11287  ccatfv0  11291  ccatval1lsw  11292  ccatval21sw  11293  lswccatn0lsw  11299  pfxsuff1eqwrdeq  11391  pfxccatid  11433  dvdsmultr1  12517  dvdssub2  12521  divalglemeuneg  12609  ndvdsadd  12617  grpsubf  13792  grpinvsub  13795  grpnpcan  13805  mulginvcom  13864  mulginvinv  13865  subgsubcl  13902  qussub  13954  ghmsub  13968  dvrcl  14280  unitdvcl  14281  basgen2  14946  opnneiss  15023  cnpf2  15072  sincosq1lem  15690