Theorem syld3an3 1318

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  syld3an1  1319  syld3an2  1320  brelrng  4963  moriotass  6002  nnncan1  8415  lediv1  9049  modqval  10586  modqvalr  10587  modqcl  10588  flqpmodeq  10589  modq0  10591  modqge0  10594  modqlt  10595  modqdiffl  10597  modqdifz  10598  modqvalp1  10605  exp3val  10803  bcval4  11014  ccatval3  11176  ccatfv0  11180  ccatval1lsw  11181  ccatval21sw  11182  lswccatn0lsw  11188  pfxsuff1eqwrdeq  11280  pfxccatid  11322  dvdsmultr1  12393  dvdssub2  12397  divalglemeuneg  12485  ndvdsadd  12493  grpsubf  13663  grpinvsub  13666  grpnpcan  13676  mulginvcom  13735  mulginvinv  13736  subgsubcl  13773  qussub  13825  ghmsub  13839  dvrcl  14151  unitdvcl  14152  basgen2  14807  opnneiss  14884  cnpf2  14933  sincosq1lem  15551