Theorem sylanl2 693

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpanlr1  718  adantlrl  732  adantlrr  733  1stconst  8096  2ndconst  8097  oesuclem  8511  oelim  8520  undom  9054  mulsub  11658  divsubdiv  11932  lcmneg  16662  vdwlem12  17053  dpjidcl  20131  mplbas2  22174  evlsvvval  22225  monmat2matmon  22962  bwth  23548  cnextfun  24202  elbl4  24701  metucn  24709  dvradcnv  26562  dchrisum0lem2a  27659  axcontlem4  29295  cnlnadjlem2  32398  chirredlem2  32721  mdsymlem5  32737  sibfof  34708  fineqvnttrclselem1  35512  relowlssretop  37987  matunitlindflem1  38245  poimirlem29  38278  unichnidl  38660  dmncan2  38706  cvrexchlem  40171  jm2.26  43709  radcnvrat  45004  binomcxplemnotnn0  45046  suplesup  46035  dvnmptdivc  46632  fourierdlem64  46864  fourierdlem74  46874  fourierdlem75  46875  fourierdlem83  46883  etransclem35  46963  iundjiun  47154  hoidmvlelem2  47290  idomcanr  49090