Theorem syld3an3 1323

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

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  10782  modqvalr  10783  modqcl  10784  flqpmodeq  10785  modq0  10787  modqge0  10790  modqlt  10791  modqdiffl  10793  modqdifz  10794  modqvalp1  10801  exp3val  10999  bcval4  11212  ccatval3  11389  ccatfv0  11393  ccatval1lsw  11394  ccatval21sw  11395  lswccatn0lsw  11401  pfxsuff1eqwrdeq  11493  pfxccatid  11535  dvdsmultr1  12623  dvdssub2  12627  divalglemeuneg  12715  ndvdsadd  12723  grpsubf  13943  grpinvsub  13946  grpnpcan  13956  mulginvcom  14009  mulginvinv  14010  subgsubcl  14047  qussub  14099  ghmsub  14113  dvrcl  14551  unitdvcl  14552  ascldimul  15140  basgen2  15307  opnneiss  15384  cnpf2  15433  sincosq1lem  16052