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  5603  fprlem1  8325  wfrlem5OLD  8353  unblem1  9328  frrlem15  9797  prodgt02  12115  lo1mul  15664  infpnlem1  16948  ghmcnp  24123  ulmcaulem  26437  ulmcau  26438  shintcli  31348  ballotlemfc0  34495  ballotlemfcc  34496  btwnxfr  36057  endofsegid  36086  bj-bary1lem1  37312  matunitlindflem1  37623  ltcvrntr  39426  poml4N  39955
  Copyright terms: Public domain W3C validator