Theorem syld3an3 1316

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 1021	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2		simp2 1022	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3		syld3an3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4		syld3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1271	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  syld3an1  1317  syld3an2  1318  brelrng  4961  moriotass  5997  nnncan1  8405  lediv1  9039  modqval  10576  modqvalr  10577  modqcl  10578  flqpmodeq  10579  modq0  10581  modqge0  10584  modqlt  10585  modqdiffl  10587  modqdifz  10588  modqvalp1  10595  exp3val  10793  bcval4  11004  ccatval3  11166  ccatfv0  11170  ccatval1lsw  11171  ccatval21sw  11172  lswccatn0lsw  11178  pfxsuff1eqwrdeq  11270  pfxccatid  11312  dvdsmultr1  12382  dvdssub2  12386  divalglemeuneg  12474  ndvdsadd  12482  grpsubf  13652  grpinvsub  13655  grpnpcan  13665  mulginvcom  13724  mulginvinv  13725  subgsubcl  13762  qussub  13814  ghmsub  13828  dvrcl  14139  unitdvcl  14140  basgen2  14795  opnneiss  14872  cnpf2  14921  sincosq1lem  15539