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  8123  2ndconst  8124  oesuclem  8561  oelim  8570  undom  9097  mulsub  11703  divsubdiv  11980  lcmneg  16636  vdwlem12  17025  dpjidcl  20092  mplbas2  22077  monmat2matmon  22845  bwth  23433  cnextfun  24087  elbl4  24591  metucn  24599  dvradcnv  26478  dchrisum0lem2a  27575  axcontlem4  28996  cnlnadjlem2  32096  chirredlem2  32419  mdsymlem5  32435  sibfof  34321  relowlssretop  37345  matunitlindflem1  37602  poimirlem29  37635  unichnidl  38017  dmncan2  38063  cvrexchlem  39401  evlsvvval  42549  jm2.26  42990  radcnvrat  44309  binomcxplemnotnn0  44351  suplesup  45288  dvnmptdivc  45893  fourierdlem64  46125  fourierdlem74  46135  fourierdlem75  46136  fourierdlem83  46144  etransclem35  46224  iundjiun  46415  hoidmvlelem2  46551