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  8025  2ndconst  8026  oesuclem  8435  oelim  8444  undom  8973  mulsub  11552  divsubdiv  11829  lcmneg  16506  vdwlem12  16896  dpjidcl  19965  mplbas2  21970  monmat2matmon  22732  bwth  23318  cnextfun  23972  elbl4  24471  metucn  24479  dvradcnv  26350  dchrisum0lem2a  27448  axcontlem4  28938  cnlnadjlem2  32038  chirredlem2  32361  mdsymlem5  32377  sibfof  34343  fineqvnttrclselem1  35109  relowlssretop  37376  matunitlindflem1  37635  poimirlem29  37668  unichnidl  38050  dmncan2  38096  cvrexchlem  39437  evlsvvval  42575  jm2.26  43014  radcnvrat  44326  binomcxplemnotnn0  44368  suplesup  45357  dvnmptdivc  45955  fourierdlem64  46187  fourierdlem74  46197  fourierdlem75  46198  fourierdlem83  46206  etransclem35  46286  iundjiun  46477  hoidmvlelem2  46613