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	adantl 481	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
3		sylanl2.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	syldanl 603	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  707  adantlrl  721  adantlrr  722  1stconst  8043  2ndconst  8044  oesuclem  8453  oelim  8462  undom  8996  mulsub  11584  divsubdiv  11862  lcmneg  16563  vdwlem12  16954  dpjidcl  20026  mplbas2  22030  evlsvvval  22081  monmat2matmon  22799  bwth  23385  cnextfun  24039  elbl4  24538  metucn  24546  dvradcnv  26399  dchrisum0lem2a  27494  axcontlem4  29050  cnlnadjlem2  32154  chirredlem2  32477  mdsymlem5  32493  sibfof  34500  fineqvnttrclselem1  35281  relowlssretop  37693  matunitlindflem1  37951  poimirlem29  37984  unichnidl  38366  dmncan2  38412  cvrexchlem  39879  jm2.26  43448  radcnvrat  44759  binomcxplemnotnn0  44801  suplesup  45787  dvnmptdivc  46384  fourierdlem64  46616  fourierdlem74  46626  fourierdlem75  46627  fourierdlem83  46635  etransclem35  46715  iundjiun  46906  hoidmvlelem2  47042