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  4969  moriotass  6012  nnncan1  8474  lediv1  9108  modqval  10649  modqvalr  10650  modqcl  10651  flqpmodeq  10652  modq0  10654  modqge0  10657  modqlt  10658  modqdiffl  10660  modqdifz  10661  modqvalp1  10668  exp3val  10866  bcval4  11077  ccatval3  11242  ccatfv0  11246  ccatval1lsw  11247  ccatval21sw  11248  lswccatn0lsw  11254  pfxsuff1eqwrdeq  11346  pfxccatid  11388  dvdsmultr1  12472  dvdssub2  12476  divalglemeuneg  12564  ndvdsadd  12572  grpsubf  13742  grpinvsub  13745  grpnpcan  13755  mulginvcom  13814  mulginvinv  13815  subgsubcl  13852  qussub  13904  ghmsub  13918  dvrcl  14230  unitdvcl  14231  basgen2  14892  opnneiss  14969  cnpf2  15018  sincosq1lem  15636