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  8036  2ndconst  8037  oesuclem  8446  oelim  8455  undom  8985  mulsub  11567  divsubdiv  11844  lcmneg  16516  vdwlem12  16906  dpjidcl  19974  mplbas2  21978  monmat2matmon  22740  bwth  23326  cnextfun  23980  elbl4  24479  metucn  24487  dvradcnv  26358  dchrisum0lem2a  27456  axcontlem4  28947  cnlnadjlem2  32050  chirredlem2  32373  mdsymlem5  32389  sibfof  34374  fineqvnttrclselem1  35162  relowlssretop  37428  matunitlindflem1  37676  poimirlem29  37709  unichnidl  38091  dmncan2  38137  cvrexchlem  39538  evlsvvval  42681  jm2.26  43119  radcnvrat  44431  binomcxplemnotnn0  44473  suplesup  45462  dvnmptdivc  46060  fourierdlem64  46292  fourierdlem74  46302  fourierdlem75  46303  fourierdlem83  46311  etransclem35  46391  iundjiun  46582  hoidmvlelem2  46718