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

Theorem syldd 70
 Description: Nested syllogism deduction. Deduction associated with syld 46. Double deduction associated with syl 17. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 11-May-2013.)
Hypotheses
Ref Expression
syldd.1 (𝜑 → (𝜓 → (𝜒𝜃)))
syldd.2 (𝜑 → (𝜓 → (𝜃𝜏)))
Assertion
Ref Expression
syldd (𝜑 → (𝜓 → (𝜒𝜏)))

Proof of Theorem syldd
StepHypRef Expression
1 syldd.2 . 2 (𝜑 → (𝜓 → (𝜃𝜏)))
2 syldd.1 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
3 imim2 56 . 2 ((𝜃𝜏) → ((𝜒𝜃) → (𝜒𝜏)))
41, 2, 3syl6c 68 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:  syl5d  71  syl6d  73  syl10  77  tfinds  6951  tz7.49  7427  dffi2  8212  ordiso2  8303  rankuni2b  8599  oddprmdvds  15445  brbtwn2  25585  soseq  30995  prtlem60  33152  lvoli2  33885
 Copyright terms: Public domain W3C validator