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  8564  lediv1  9202  ind1  9303  modqval  10776  modqvalr  10777  modqcl  10778  flqpmodeq  10779  modq0  10781  modqge0  10784  modqlt  10785  modqdiffl  10787  modqdifz  10788  modqvalp1  10795  exp3val  10993  bcval4  11206  ccatval3  11383  ccatfv0  11387  ccatval1lsw  11388  ccatval21sw  11389  lswccatn0lsw  11395  pfxsuff1eqwrdeq  11487  pfxccatid  11529  dvdsmultr1  12617  dvdssub2  12621  divalglemeuneg  12709  ndvdsadd  12717  grpsubf  13937  grpinvsub  13940  grpnpcan  13950  mulginvcom  14003  mulginvinv  14004  subgsubcl  14041  qussub  14093  ghmsub  14107  dvrcl  14526  unitdvcl  14527  ascldimul  15115  basgen2  15273  opnneiss  15350  cnpf2  15399  sincosq1lem  16018