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 591 . 2 ((𝜒𝜑) → (𝜒𝜃))
3 sylanr2.2 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
42, 3sylan2 490 1 ((𝜓 ∧ (𝜒𝜑)) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  adantrrl  756  adantrrr  757  1stconst  7152  2ndconst  7153  isfin7-2  9101  mulsub  10352  fzsubel  12248  expsub  12770  ramlb  15561  0ram  15562  ressmplvsca  19280  tgcl  20584  fgss2  21488  nmoid  22356  chirredlem4  28636  poimirlem28  32607  pridlc3  33042  stoweidlem34  38927
 Copyright terms: Public domain W3C validator