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

Theorem sylanr2 682
 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 619 . 2 ((𝜒𝜑) → (𝜒𝜃))
3 sylanr2.2 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
42, 3sylan2 595 1 ((𝜓 ∧ (𝜒𝜑)) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  adantrrl  723  adantrrr  724  isfin7-2  9809  mulsub  11074  fzsubel  12940  expsub  13475  ramlb  16347  0ram  16348  ressmplvsca  20703  tgcl  21581  fgss2  22486  nmoid  23355  numclwwlkqhash  28167  chirredlem4  30183  pibt2  34850  lindsadd  35066  poimirlem28  35101  pridlc3  35527  stoweidlem34  42691
 Copyright terms: Public domain W3C validator