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  8079  2ndconst  8080  oesuclem  8489  oelim  8498  undom  9029  mulsub  11621  divsubdiv  11898  lcmneg  16573  vdwlem12  16963  dpjidcl  19990  mplbas2  21949  monmat2matmon  22711  bwth  23297  cnextfun  23951  elbl4  24451  metucn  24459  dvradcnv  26330  dchrisum0lem2a  27428  axcontlem4  28894  cnlnadjlem2  31997  chirredlem2  32320  mdsymlem5  32336  sibfof  34331  relowlssretop  37351  matunitlindflem1  37610  poimirlem29  37643  unichnidl  38025  dmncan2  38071  cvrexchlem  39413  evlsvvval  42551  jm2.26  42991  radcnvrat  44303  binomcxplemnotnn0  44345  suplesup  45335  dvnmptdivc  45936  fourierdlem64  46168  fourierdlem74  46178  fourierdlem75  46179  fourierdlem83  46187  etransclem35  46267  iundjiun  46458  hoidmvlelem2  46594