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  3853  bropfvvvv  8078  wfrlem12OLD  8320  tfrlem9  8385  axcc2lem  10431  axdc3lem4  10448  fpwwe2lem7  10632  tskcard  10776  nqereu  10924  lbzbi  12920  fleqceilz  13819  ndvdsadd  16353  gcdneg  16463  ulmcaulem  25906  wlkiswwlks1  29121  elwspths2on  29214  relowlpssretop  36245  poimirlem18  36506  heicant  36523  brabg2  36585  neificl  36621  el1fzopredsuc  46033
  Copyright terms: Public domain W3C validator