Theorem syld3an3 1323

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 1028	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2		simp2 1029	. 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 1278	1 |- ( ( ph /\ ps /\ ch ) -> ta )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syld3an1  1324  syld3an2  1325  brelrng  5013  moriotass  6069  nnncan1  8562  lediv1  9199  ind1  9300  modqval  10761  modqvalr  10762  modqcl  10763  flqpmodeq  10764  modq0  10766  modqge0  10769  modqlt  10770  modqdiffl  10772  modqdifz  10773  modqvalp1  10780  exp3val  10978  bcval4  11190  ccatval3  11367  ccatfv0  11371  ccatval1lsw  11372  ccatval21sw  11373  lswccatn0lsw  11379  pfxsuff1eqwrdeq  11471  pfxccatid  11513  dvdsmultr1  12598  dvdssub2  12602  divalglemeuneg  12690  ndvdsadd  12698  grpsubf  13884  grpinvsub  13887  grpnpcan  13897  mulginvcom  13950  mulginvinv  13951  subgsubcl  13988  qussub  14040  ghmsub  14054  dvrcl  14442  unitdvcl  14443  ascldimul  15031  basgen2  15182  opnneiss  15259  cnpf2  15308  sincosq1lem  15926