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

Theorem sylanr2 679
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 616 . 2 ((𝜒𝜑) → (𝜒𝜃))
3 sylanr2.2 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
42, 3sylan2 592 1 ((𝜓 ∧ (𝜒𝜑)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  adantrrl  720  adantrrr  721  isfin7-2  9806  mulsub  11071  fzsubel  12931  expsub  13465  ramlb  16343  0ram  16344  ressmplvsca  20168  tgcl  21505  fgss2  22410  nmoid  23278  numclwwlkqhash  28081  chirredlem4  30097  pibt2  34580  lindsadd  34766  poimirlem28  34801  pridlc3  35232  stoweidlem34  42196
  Copyright terms: Public domain W3C validator