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

Theorem mpdi 45
 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 43 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  46  pm2.43d  53  impt  169  sbcimdv  3484  predpo  5662  suctrOLD  5773  bropfvvvv  7209  wfrlem12  7378  tfrlem9  7433  axcc2lem  9210  axdc3lem4  9227  fpwwe2lem8  9411  tskcard  9555  nqereu  9703  lbzbi  11728  fleqceilz  12601  ndvdsadd  15069  gcdneg  15178  ulmcaulem  24069  wlkiswwlks1  26639  frgrwopreglem4  27059  frrlem11  31528  relowlpssretop  32879  poimirlem18  33094  heicant  33111  brabg2  33177  neificl  33216  el1fzopredsuc  40658
 Copyright terms: Public domain W3C validator