MPE Home 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  fvf1pr  7327  tfinds  7881  soseq  8183  tz7.49  8484  php3  9247  dffi2  9461  ordiso2  9553  rankuni2b  9891  oddprmdvds  16937  brbtwn2  28935  bj-exalims  36617  prtlem60  38835  lvoli2  39564
  Copyright terms: Public domain W3C validator