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

Theorem sylanr2 683
Description: A syllogism inference. (Contributed by NM, 9-Apr-2005.)
Hypotheses
Ref Expression
sylanr2.1 (𝜑𝜃)
sylanr2.2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
sylanr2 ((𝜓 ∧ (𝜒𝜑)) → 𝜏)

Proof of Theorem sylanr2
StepHypRef Expression
1 sylanr2.1 . . 3 (𝜑𝜃)
21anim2i 617 . 2 ((𝜒𝜑) → (𝜒𝜃))
3 sylanr2.2 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
42, 3sylan2 593 1 ((𝜓 ∧ (𝜒𝜑)) → 𝜏)
Colors of variables: wff setvar class
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:  adantrrl  724  adantrrr  725  unfi  9210  isfin7-2  10434  mulsub  11704  fzsubel  13597  expsub  14148  ramlb  17053  0ram  17054  ressmplvsca  22067  tgcl  22992  fgss2  23898  nmoid  24779  madebdaylemlrcut  27952  numclwwlkqhash  30404  chirredlem4  32422  pibt2  37400  lindsadd  37600  poimirlem28  37635  pridlc3  38060  stoweidlem34  45990
  Copyright terms: Public domain W3C validator