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

Theorem mpdi 44
 Description: A nested modus ponens deduction. (Contributed by NM, 16-Apr-2005.) (Proof shortened by Mel L. O'Cat, 15-Jan-2008.)
Hypotheses
Ref Expression
mpdi.1 (𝜓𝜒)
mpdi.2 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
mpdi (𝜑 → (𝜓𝜃))

Proof of Theorem mpdi
StepHypRef Expression
1 mpdi.1 . . 3 (𝜓𝜒)
21a1i 11 . 2 (𝜑 → (𝜓𝜒))
3 mpdi.2 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
42, 3mpdd 42 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:  mpii  45  pm2.43d  51  impt  168  sbcimdv  3465  predpo  5615  suctrOLD  5726  bropfvvvv  7144  wfrlem12  7313  tfrlem9  7368  axcc2lem  9141  axdc3lem4  9158  fpwwe2lem8  9338  tskcard  9482  nqereu  9630  lbzbi  11652  fleqceilz  12515  ndvdsadd  14972  gcdneg  15081  ulmcaulem  23952  wlkiswwlk1  26218  frgrawopreglem4  26574  frrlem11  31036  relowlpssretop  32388  poimirlem18  32597  heicant  32614  brabg2  32680  neificl  32719  el1fzopredsuc  39948  frgrwopreglem4  41484
 Copyright terms: Public domain W3C validator