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  7774  oelim  7783  mulsub  10665  divsubdiv  10933  lcmneg  15518  vdwlem12  15898  dpjidcl  18657  mplbas2  19672  monmat2matmon  20831  bwth  21415  cnextfun  22069  elbl4  22569  metucn  22577  dvradcnv  24374  dchrisum0lem2a  25405  axcontlem4  26046  cnlnadjlem2  29236  chirredlem2  29559  mdsymlem5  29575  sibfof  30711  relowlssretop  33522  matunitlindflem1  33718  poimirlem29  33751  unichnidl  34143  dmncan2  34189  cvrexchlem  35208  jm2.26  38071  radcnvrat  39015  binomcxplemnotnn0  39057  suplesup  40053  dvnmptdivc  40656  fourierdlem64  40890  fourierdlem74  40900  fourierdlem75  40901  fourierdlem83  40909  etransclem35  40989  iundjiun  41180  hoidmvlelem2  41316
  Copyright terms: Public domain W3C validator