MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylanl2 Structured version   Visualization version   GIF version

Theorem sylanl2 672
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
StepHypRef Expression
1 sylanl2.1 . . 3 (𝜑𝜒)
21anim2i 611 . 2 ((𝜓𝜑) → (𝜓𝜒))
3 sylanl2.2 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
42, 3sylan 576 1 (((𝜓𝜑) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385
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 199  df-an 386
This theorem is referenced by:  mpanlr1  698  adantlrl  712  adantlrr  713  1stconst  7502  2ndconst  7503  oesuclem  7845  oelim  7854  mulsub  10765  divsubdiv  11033  lcmneg  15651  vdwlem12  16029  dpjidcl  18773  mplbas2  19793  monmat2matmon  20957  bwth  21542  cnextfun  22196  elbl4  22696  metucn  22704  dvradcnv  24516  dchrisum0lem2a  25558  axcontlem4  26204  cnlnadjlem2  29452  chirredlem2  29775  mdsymlem5  29791  sibfof  30918  relowlssretop  33709  matunitlindflem1  33894  poimirlem29  33927  unichnidl  34317  dmncan2  34363  cvrexchlem  35440  jm2.26  38354  radcnvrat  39295  binomcxplemnotnn0  39337  suplesup  40299  dvnmptdivc  40897  fourierdlem64  41130  fourierdlem74  41140  fourierdlem75  41141  fourierdlem83  41149  etransclem35  41229  iundjiun  41420  hoidmvlelem2  41556
  Copyright terms: Public domain W3C validator