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  8040  2ndconst  8041  oesuclem  8450  oelim  8459  undom  8989  mulsub  11581  divsubdiv  11858  lcmneg  16532  vdwlem12  16922  dpjidcl  19957  mplbas2  21965  monmat2matmon  22727  bwth  23313  cnextfun  23967  elbl4  24467  metucn  24475  dvradcnv  26346  dchrisum0lem2a  27444  axcontlem4  28930  cnlnadjlem2  32030  chirredlem2  32353  mdsymlem5  32369  sibfof  34307  relowlssretop  37336  matunitlindflem1  37595  poimirlem29  37628  unichnidl  38010  dmncan2  38056  cvrexchlem  39398  evlsvvval  42536  jm2.26  42975  radcnvrat  44287  binomcxplemnotnn0  44329  suplesup  45319  dvnmptdivc  45920  fourierdlem64  46152  fourierdlem74  46162  fourierdlem75  46163  fourierdlem83  46171  etransclem35  46251  iundjiun  46442  hoidmvlelem2  46578