MPE Home 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  181  sbcimdv  3789  predpo  6134  bropfvvvv  7770  wfrlem12  7949  tfrlem9  8004  axcc2lem  9847  axdc3lem4  9864  fpwwe2lem8  10048  tskcard  10192  nqereu  10340  lbzbi  12324  fleqceilz  13217  ndvdsadd  15751  gcdneg  15860  ulmcaulem  24989  wlkiswwlks1  27653  elwspths2on  27746  relowlpssretop  34781  poimirlem18  35075  heicant  35092  brabg2  35154  neificl  35191  el1fzopredsuc  43880
  Copyright terms: Public domain W3C validator