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  5991  nnncan1  8393  lediv1  9027  modqval  10558  modqvalr  10559  modqcl  10560  flqpmodeq  10561  modq0  10563  modqge0  10566  modqlt  10567  modqdiffl  10569  modqdifz  10570  modqvalp1  10577  exp3val  10775  bcval4  10986  ccatval3  11147  ccatfv0  11151  ccatval1lsw  11152  ccatval21sw  11153  lswccatn0lsw  11159  pfxsuff1eqwrdeq  11247  pfxccatid  11289  dvdsmultr1  12358  dvdssub2  12362  divalglemeuneg  12450  ndvdsadd  12458  grpsubf  13628  grpinvsub  13631  grpnpcan  13641  mulginvcom  13700  mulginvinv  13701  subgsubcl  13738  qussub  13790  ghmsub  13804  dvrcl  14115  unitdvcl  14116  basgen2  14771  opnneiss  14848  cnpf2  14897  sincosq1lem  15515