Theorem sylanl2 681

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 602	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  706  adantlrl  720  adantlrr  721  1stconst  8082  2ndconst  8083  oesuclem  8492  oelim  8501  undom  9033  mulsub  11628  divsubdiv  11905  lcmneg  16580  vdwlem12  16970  dpjidcl  19997  mplbas2  21956  monmat2matmon  22718  bwth  23304  cnextfun  23958  elbl4  24458  metucn  24466  dvradcnv  26337  dchrisum0lem2a  27435  axcontlem4  28901  cnlnadjlem2  32004  chirredlem2  32327  mdsymlem5  32343  sibfof  34338  relowlssretop  37358  matunitlindflem1  37617  poimirlem29  37650  unichnidl  38032  dmncan2  38078  cvrexchlem  39420  evlsvvval  42558  jm2.26  42998  radcnvrat  44310  binomcxplemnotnn0  44352  suplesup  45342  dvnmptdivc  45943  fourierdlem64  46175  fourierdlem74  46185  fourierdlem75  46186  fourierdlem83  46194  etransclem35  46274  iundjiun  46465  hoidmvlelem2  46601