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  178  sbcimdvOLD  3812  bropfvvvv  8016  wfrlem12OLD  8258  tfrlem9  8323  axcc2lem  10330  axdc3lem4  10347  fpwwe2lem7  10531  tskcard  10675  nqereu  10823  lbzbi  12815  fleqceilz  13713  ndvdsadd  16251  gcdneg  16361  ulmcaulem  25704  wlkiswwlks1  28640  elwspths2on  28733  relowlpssretop  35766  poimirlem18  36027  heicant  36044  brabg2  36106  neificl  36143  el1fzopredsuc  45451
  Copyright terms: Public domain W3C validator