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  5015  moriotass  6072  nnncan1  8569  lediv1  9207  ind1  9309  modqval  10781  modqvalr  10782  modqcl  10783  flqpmodeq  10784  modq0  10786  modqge0  10789  modqlt  10790  modqdiffl  10792  modqdifz  10793  modqvalp1  10800  exp3val  10998  bcval4  11211  ccatval3  11388  ccatfv0  11392  ccatval1lsw  11393  ccatval21sw  11394  lswccatn0lsw  11400  pfxsuff1eqwrdeq  11492  pfxccatid  11534  dvdsmultr1  12622  dvdssub2  12626  divalglemeuneg  12714  ndvdsadd  12722  grpsubf  13942  grpinvsub  13945  grpnpcan  13955  mulginvcom  14008  mulginvinv  14009  subgsubcl  14046  qussub  14098  ghmsub  14112  dvrcl  14550  unitdvcl  14551  ascldimul  15139  basgen2  15324  opnneiss  15401  cnpf2  15450  sincosq1lem  16069