Theorem syld3an3 1295

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 1000	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2		simp2 1001	. 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 1250	1 |- ( ( ph /\ ps /\ ch ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  syld3an1  1296  syld3an2  1297  brelrng  4909  moriotass  5928  nnncan1  8308  lediv1  8942  modqval  10469  modqvalr  10470  modqcl  10471  flqpmodeq  10472  modq0  10474  modqge0  10477  modqlt  10478  modqdiffl  10480  modqdifz  10481  modqvalp1  10488  exp3val  10686  bcval4  10897  ccatval3  11055  ccatfv0  11059  ccatval1lsw  11060  ccatval21sw  11061  lswccatn0lsw  11067  dvdsmultr1  12142  dvdssub2  12146  divalglemeuneg  12234  ndvdsadd  12242  grpsubf  13411  grpinvsub  13414  grpnpcan  13424  mulginvcom  13483  mulginvinv  13484  subgsubcl  13521  qussub  13573  ghmsub  13587  dvrcl  13897  unitdvcl  13898  basgen2  14553  opnneiss  14630  cnpf2  14679  sincosq1lem  15297