Theorem syld3an3 1319

Description: A syllogism inference. (Contributed by NM, 20-May-2007.)

Hypotheses

Ref	Expression
syld3an3.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
syld3an3.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syld3an3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Proof of Theorem syld3an3

Step	Hyp	Ref	Expression
1		simp1 1024	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2		simp2 1025	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3		syld3an3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4		syld3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1274	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  syld3an1  1320  syld3an2  1321  brelrng  4993  moriotass  6042  nnncan1  8525  lediv1  9160  modqval  10710  modqvalr  10711  modqcl  10712  flqpmodeq  10713  modq0  10715  modqge0  10718  modqlt  10719  modqdiffl  10721  modqdifz  10722  modqvalp1  10729  exp3val  10927  bcval4  11139  ccatval3  11312  ccatfv0  11316  ccatval1lsw  11317  ccatval21sw  11318  lswccatn0lsw  11324  pfxsuff1eqwrdeq  11416  pfxccatid  11458  dvdsmultr1  12542  dvdssub2  12546  divalglemeuneg  12634  ndvdsadd  12642  grpsubf  13834  grpinvsub  13837  grpnpcan  13847  mulginvcom  13900  mulginvinv  13901  subgsubcl  13938  qussub  13990  ghmsub  14004  dvrcl  14380  unitdvcl  14381  basgen2  15072  opnneiss  15149  cnpf2  15198  sincosq1lem  15816