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

Theorem sylanr2 665
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 605 . 2 ((𝜒𝜑) → (𝜒𝜃))
3 sylanr2.2 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
42, 3sylan2 582 1 ((𝜓 ∧ (𝜒𝜑)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  adantrrl  706  adantrrr  707  1stconst  7493  2ndconst  7494  isfin7-2  9497  mulsub  10752  fzsubel  12594  expsub  13125  ramlb  15934  0ram  15935  ressmplvsca  19662  tgcl  20981  fgss2  21885  nmoid  22753  numclwwlkqhash  27549  chirredlem4  29574  poimirlem28  33744  pridlc3  34177  stoweidlem34  40724
  Copyright terms: Public domain W3C validator