Theorem syld3an3 1318

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  syld3an1  1319  syld3an2  1320  brelrng  4963  moriotass  6001  nnncan1  8414  lediv1  9048  modqval  10585  modqvalr  10586  modqcl  10587  flqpmodeq  10588  modq0  10590  modqge0  10593  modqlt  10594  modqdiffl  10596  modqdifz  10597  modqvalp1  10604  exp3val  10802  bcval4  11013  ccatval3  11175  ccatfv0  11179  ccatval1lsw  11180  ccatval21sw  11181  lswccatn0lsw  11187  pfxsuff1eqwrdeq  11279  pfxccatid  11321  dvdsmultr1  12391  dvdssub2  12395  divalglemeuneg  12483  ndvdsadd  12491  grpsubf  13661  grpinvsub  13664  grpnpcan  13674  mulginvcom  13733  mulginvinv  13734  subgsubcl  13771  qussub  13823  ghmsub  13837  dvrcl  14148  unitdvcl  14149  basgen2  14804  opnneiss  14881  cnpf2  14930  sincosq1lem  15548