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  8030  2ndconst  8031  oesuclem  8440  oelim  8449  undom  8978  mulsub  11557  divsubdiv  11834  lcmneg  16511  vdwlem12  16901  dpjidcl  19970  mplbas2  21975  monmat2matmon  22737  bwth  23323  cnextfun  23977  elbl4  24476  metucn  24484  dvradcnv  26355  dchrisum0lem2a  27453  axcontlem4  28943  cnlnadjlem2  32043  chirredlem2  32366  mdsymlem5  32382  sibfof  34348  fineqvnttrclselem1  35129  relowlssretop  37396  matunitlindflem1  37655  poimirlem29  37688  unichnidl  38070  dmncan2  38116  cvrexchlem  39457  evlsvvval  42595  jm2.26  43034  radcnvrat  44346  binomcxplemnotnn0  44388  suplesup  45377  dvnmptdivc  45975  fourierdlem64  46207  fourierdlem74  46217  fourierdlem75  46218  fourierdlem83  46226  etransclem35  46306  iundjiun  46497  hoidmvlelem2  46633