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  8097  2ndconst  8098  oesuclem  8535  oelim  8544  undom  9071  mulsub  11678  divsubdiv  11955  lcmneg  16620  vdwlem12  17010  dpjidcl  20039  mplbas2  21998  monmat2matmon  22760  bwth  23346  cnextfun  24000  elbl4  24500  metucn  24508  dvradcnv  26380  dchrisum0lem2a  27478  axcontlem4  28892  cnlnadjlem2  31995  chirredlem2  32318  mdsymlem5  32334  sibfof  34318  relowlssretop  37327  matunitlindflem1  37586  poimirlem29  37619  unichnidl  38001  dmncan2  38047  cvrexchlem  39384  evlsvvval  42533  jm2.26  42973  radcnvrat  44286  binomcxplemnotnn0  44328  suplesup  45314  dvnmptdivc  45915  fourierdlem64  46147  fourierdlem74  46157  fourierdlem75  46158  fourierdlem83  46166  etransclem35  46246  iundjiun  46437  hoidmvlelem2  46573