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

Theorem sylan2d 499
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 470 . . 3 (𝜑 → ((𝜒𝜃) → 𝜏))
41, 3syland 498 . 2 (𝜑 → ((𝜓𝜃) → 𝜏))
54ancomsd 470 1 (𝜑 → ((𝜃𝜓) → 𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  syl2and  500  sylan2i  686  swopo  5015  wfrlem5  7379  unblem1  8172  unfi  8187  prodgt02  10829  prodge02  10831  lo1mul  14308  infpnlem1  15557  ghmcnp  21858  ulmcaulem  24086  ulmcau  24087  shintcli  28076  ballotlemfc0  30377  ballotlemfcc  30378  frrlem5  31538  btwnxfr  31858  endofsegid  31887  bj-bary1lem1  32833  matunitlindflem1  33076  ltcvrntr  34229  poml4N  34758
  Copyright terms: Public domain W3C validator