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

Theorem syldd 72
 Description: Nested syllogism deduction. Deduction associated with syld 47. 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 58 . 2 ((𝜃𝜏) → ((𝜒𝜃) → (𝜒𝜏)))
41, 2, 3syl6c 70 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  73  syl6d  75  syl10  79  tfinds  7210  tz7.49  7697  dffi2  8489  ordiso2  8580  rankuni2b  8884  oddprmdvds  15814  brbtwn2  26006  soseq  32091  bj-exalims  32950  prtlem60  34660  lvoli2  35390
 Copyright terms: Public domain W3C validator