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  169  sbcimdv  3531  predpo  5736  suctrOLD  5847  bropfvvvv  7302  wfrlem12  7471  tfrlem9  7526  axcc2lem  9296  axdc3lem4  9313  fpwwe2lem8  9497  tskcard  9641  nqereu  9789  lbzbi  11814  fleqceilz  12693  ndvdsadd  15181  gcdneg  15290  ulmcaulem  24193  wlkiswwlks1  26821  elwspths2on  26926  relowlpssretop  33342  poimirlem18  33557  heicant  33574  brabg2  33640  neificl  33679  el1fzopredsuc  41660
  Copyright terms: Public domain W3C validator