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  9664  mulsub  10931  fzsubel  12793  expsub  13327  ramlb  16184  0ram  16185  ressmplvsca  19927  tgcl  21261  fgss2  22166  nmoid  23034  numclwwlkqhash  27846  chirredlem4  29861  pibt2  34229  lindsadd  34416  poimirlem28  34451  pridlc3  34883  stoweidlem34  41861
  Copyright terms: Public domain W3C validator