Theorem sylanl2 694

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpanlr1  719  adantlrl  733  adantlrr  734  1stconst  8101  2ndconst  8102  oesuclem  8516  oelim  8525  undom  9067  mulsub  11685  divsubdiv  11959  lcmneg  16699  vdwlem12  17090  dpjidcl  20193  mplbas2  22264  evlsvvval  22315  matunitlindflem1  22907  monmat2matmon  23055  bwth  23641  cnextfun  24296  elbl4  24795  metucn  24803  dvradcnv  26664  dchrisum0lem2a  27761  axcontlem4  29432  cnlnadjlem2  32557  chirredlem2  32880  mdsymlem5  32896  sibfof  34859  fineqvnttrclselem1  35655  relowlssretop  38125  poimirlem29  38406  unichnidl  38789  dmncan2  38835  cvrexchlem  40300  jm2.26  43851  radcnvrat  45146  binomcxplemnotnn0  45188  suplesup  46177  dvnmptdivc  46774  fourierdlem64  47006  fourierdlem74  47016  fourierdlem75  47017  fourierdlem83  47025  etransclem35  47105  iundjiun  47296  hoidmvlelem2  47432  idomcanr  49271