Theorem syld3an3 1316

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 1021	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2		simp2 1022	. 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 1271	1 |- ( ( ph /\ ps /\ ch ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  syld3an1  1317  syld3an2  1318  brelrng  4955  moriotass  5985  nnncan1  8382  lediv1  9016  modqval  10546  modqvalr  10547  modqcl  10548  flqpmodeq  10549  modq0  10551  modqge0  10554  modqlt  10555  modqdiffl  10557  modqdifz  10558  modqvalp1  10565  exp3val  10763  bcval4  10974  ccatval3  11134  ccatfv0  11138  ccatval1lsw  11139  ccatval21sw  11140  lswccatn0lsw  11146  pfxsuff1eqwrdeq  11231  pfxccatid  11273  dvdsmultr1  12342  dvdssub2  12346  divalglemeuneg  12434  ndvdsadd  12442  grpsubf  13612  grpinvsub  13615  grpnpcan  13625  mulginvcom  13684  mulginvinv  13685  subgsubcl  13722  qussub  13774  ghmsub  13788  dvrcl  14099  unitdvcl  14100  basgen2  14755  opnneiss  14832  cnpf2  14881  sincosq1lem  15499