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  2623  isofrlem  7360  kmlem9  10197  squeeze0  12169  lcmfunsnlem1  16671  rnglidlmcl  21244  fgss2  23898  ordcmp  36430  linepsubN  39735  pmapsub  39751  ichreuopeq  47398  bgoldbnnsum3prm  47729  grimedg  47841
  Copyright terms: Public domain W3C validator