Theorem sylanl2 680

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	adantl 481	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
3		sylanl2.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	syldanl 601	1 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpanlr1  705  adantlrl  719  adantlrr  720  1stconst  8141  2ndconst  8142  oesuclem  8581  oelim  8590  undom  9125  mulsub  11733  divsubdiv  12010  lcmneg  16650  vdwlem12  17039  dpjidcl  20102  mplbas2  22083  monmat2matmon  22851  bwth  23439  cnextfun  24093  elbl4  24597  metucn  24605  dvradcnv  26482  dchrisum0lem2a  27579  axcontlem4  29000  cnlnadjlem2  32100  chirredlem2  32423  mdsymlem5  32439  sibfof  34305  relowlssretop  37329  matunitlindflem1  37576  poimirlem29  37609  unichnidl  37991  dmncan2  38037  cvrexchlem  39376  evlsvvval  42518  jm2.26  42959  radcnvrat  44283  binomcxplemnotnn0  44325  suplesup  45254  dvnmptdivc  45859  fourierdlem64  46091  fourierdlem74  46101  fourierdlem75  46102  fourierdlem83  46110  etransclem35  46190  iundjiun  46381  hoidmvlelem2  46517