Theorem sylanl2 691

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mpanlr1  716  adantlrl  730  adantlrr  731  1stconst  8074  2ndconst  8075  oesuclem  8489  oelim  8498  undom  9033  mulsub  11627  divsubdiv  11904  lcmneg  16620  vdwlem12  17011  dpjidcl  20083  mplbas2  22075  evlsvvval  22126  monmat2matmon  22864  bwth  23450  cnextfun  24104  elbl4  24603  metucn  24611  dvradcnv  26461  dchrisum0lem2a  27558  axcontlem4  29114  cnlnadjlem2  32217  chirredlem2  32540  mdsymlem5  32556  sibfof  34598  fineqvnttrclselem1  35381  relowlssretop  37821  matunitlindflem1  38079  poimirlem29  38112  unichnidl  38494  dmncan2  38540  cvrexchlem  40007  jm2.26  43543  radcnvrat  44854  binomcxplemnotnn0  44896  suplesup  45879  dvnmptdivc  46476  fourierdlem64  46708  fourierdlem74  46718  fourierdlem75  46719  fourierdlem83  46727  etransclem35  46807  iundjiun  46998  hoidmvlelem2  47134