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

Theorem syl5d 73
Description: A nested syllogism deduction. Deduction associated with syl5 34. (Contributed by NM, 14-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) (Proof shortened by Mel L. O'Cat, 2-Feb-2006.)
Hypotheses
Ref Expression
syl5d.1 (𝜑 → (𝜓𝜒))
syl5d.2 (𝜑 → (𝜃 → (𝜒𝜏)))
Assertion
Ref Expression
syl5d (𝜑 → (𝜃 → (𝜓𝜏)))

Proof of Theorem syl5d
StepHypRef Expression
1 syl5d.1 . . 3 (𝜑 → (𝜓𝜒))
21a1d 25 . 2 (𝜑 → (𝜃 → (𝜓𝜒)))
3 syl5d.2 . 2 (𝜑 → (𝜃 → (𝜒𝜏)))
42, 3syldd 72 1 (𝜑 → (𝜃 → (𝜓𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl7  74  syl9  77  imim12d  81  sbi1OLD  2544  sbi1ALT  2608  mopick  2713  isofrlem  7075  kmlem9  9569  squeeze0  11528  lcmfunsnlem1  15968  fgss2  22468  ordcmp  33813  linepsubN  36948  pmapsub  36964  ichreuopeq  43832  bgoldbnnsum3prm  44164
  Copyright terms: Public domain W3C validator