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

Theorem sylan2d 500
 Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
Hypotheses
Ref Expression
sylan2d.1 (𝜑 → (𝜓𝜒))
sylan2d.2 (𝜑 → ((𝜃𝜒) → 𝜏))
Assertion
Ref Expression
sylan2d (𝜑 → ((𝜃𝜓) → 𝜏))

Proof of Theorem sylan2d
StepHypRef Expression
1 sylan2d.1 . . 3 (𝜑 → (𝜓𝜒))
2 sylan2d.2 . . . 4 (𝜑 → ((𝜃𝜒) → 𝜏))
32ancomsd 469 . . 3 (𝜑 → ((𝜒𝜃) → 𝜏))
41, 3syland 499 . 2 (𝜑 → ((𝜓𝜃) → 𝜏))
54ancomsd 469 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 197  df-an 385 This theorem is referenced by:  syl2and  501  sylan2i  690  swopo  5197  wfrlem5  7589  unblem1  8379  unfi  8394  prodgt02  11081  prodge02  11083  lo1mul  14577  infpnlem1  15836  ghmcnp  22139  ulmcaulem  24367  ulmcau  24368  shintcli  28518  ballotlemfc0  30884  ballotlemfcc  30885  frrlem5  32111  btwnxfr  32490  endofsegid  32519  bj-bary1lem1  33490  matunitlindflem1  33736  ltcvrntr  35231  poml4N  35760
 Copyright terms: Public domain W3C validator