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

Theorem sylanl2 686
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 594 . 2 ((𝜓𝜑) → (𝜓𝜒))
3 sylanl2.2 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
42, 3sylan 489 1 (((𝜓𝜑) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  mpanlr1  724  adantlrl  758  adantlrr  759  oesuclem  7772  oelim  7781  mulsub  10663  divsubdiv  10931  lcmneg  15516  vdwlem12  15896  dpjidcl  18655  mplbas2  19670  monmat2matmon  20829  bwth  21413  cnextfun  22067  elbl4  22567  metucn  22575  dvradcnv  24372  dchrisum0lem2a  25403  axcontlem4  26044  cnlnadjlem2  29234  chirredlem2  29557  mdsymlem5  29573  sibfof  30709  relowlssretop  33520  matunitlindflem1  33716  poimirlem29  33749  unichnidl  34141  dmncan2  34187  cvrexchlem  35206  jm2.26  38069  radcnvrat  39013  binomcxplemnotnn0  39055  suplesup  40051  dvnmptdivc  40654  fourierdlem64  40888  fourierdlem74  40898  fourierdlem75  40899  fourierdlem83  40907  etransclem35  40987  iundjiun  41178  hoidmvlelem2  41314
  Copyright terms: Public domain W3C validator