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  mopick  2613  isofrlem  7330  kmlem9  10150  squeeze0  12116  lcmfunsnlem1  16577  rnglidlmcl  21071  fgss2  23722  ordcmp  35832  linepsubN  39126  pmapsub  39142  ichreuopeq  46686  bgoldbnnsum3prm  47017
  Copyright terms: Public domain W3C validator