Theorem sylanl2 682

Description: A syllogism inference. (Contributed by NM, 1-Jan-2005.)

Hypotheses

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

Assertion

Ref	Expression
sylanl2	⊢ (((𝜓 ∧ 𝜑) ∧ 𝜃) → 𝜏)

Proof of Theorem sylanl2

Step	Hyp	Ref	Expression
1		sylanl2.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	anim2i 592	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜓 ∧ 𝜒))
3		sylanl2.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylan 488	1 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  mpanlr1  721  adantlrl  755  adantlrr  756  oesuclem  7550  oelim  7559  mulsub  10417  divsubdiv  10685  lcmneg  15240  vdwlem12  15620  dpjidcl  18378  mplbas2  19389  monmat2matmon  20548  bwth  21123  cnextfun  21778  elbl4  22278  metucn  22286  dvradcnv  24079  dchrisum0lem2a  25106  axcontlem4  25747  cnlnadjlem2  28773  chirredlem2  29096  mdsymlem5  29112  sibfof  30180  relowlssretop  32840  matunitlindflem1  33034  poimirlem29  33067  unichnidl  33459  dmncan2  33505  cvrexchlem  34182  jm2.26  37046  radcnvrat  37992  binomcxplemnotnn0  38034  suplesup  39016  dvnmptdivc  39456  fourierdlem64  39691  fourierdlem74  39701  fourierdlem75  39702  fourierdlem83  39710  etransclem35  39790  iundjiun  39981  hoidmvlelem2  40114