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

Theorem sylan2d 605
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 465 . . 3 (𝜑 → ((𝜒𝜃) → 𝜏))
41, 3syland 603 . 2 (𝜑 → ((𝜓𝜃) → 𝜏))
54ancomsd 465 1 (𝜑 → ((𝜃𝜓) → 𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  sylan2i  606  syl2and  608  swopo  5608  fprlem1  8324  wfrlem5OLD  8352  unblem1  9326  frrlem15  9795  prodgt02  12113  lo1mul  15661  infpnlem1  16944  ghmcnp  24139  ulmcaulem  26452  ulmcau  26453  shintcli  31358  ballotlemfc0  34474  ballotlemfcc  34475  btwnxfr  36038  endofsegid  36067  bj-bary1lem1  37294  matunitlindflem1  37603  ltcvrntr  39407  poml4N  39936
  Copyright terms: Public domain W3C validator