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  170  sbcimdv  3695  predpo  5911  suctrOLD  6022  bropfvvvv  7491  wfrlem12  7662  tfrlem9  7717  axcc2lem  9543  axdc3lem4  9560  fpwwe2lem8  9744  tskcard  9888  nqereu  10036  lbzbi  11995  fleqceilz  12877  ndvdsadd  15353  gcdneg  15462  ulmcaulem  24362  wlkiswwlks1  26994  elwspths2on  27101  relowlpssretop  33528  poimirlem18  33740  heicant  33757  brabg2  33822  neificl  33860  el1fzopredsuc  41910
  Copyright terms: Public domain W3C validator