MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp2d Structured version   Visualization version   GIF version

Theorem mp2d 49
Description: A double modus ponens deduction. Deduction associated with mp2 9. (Contributed by NM, 23-May-2013.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
Hypotheses
Ref Expression
mp2d.1 (𝜑𝜓)
mp2d.2 (𝜑𝜒)
mp2d.3 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
mp2d (𝜑𝜃)

Proof of Theorem mp2d
StepHypRef Expression
1 mp2d.1 . 2 (𝜑𝜓)
2 mp2d.2 . . 3 (𝜑𝜒)
3 mp2d.3 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
42, 3mpid 44 . 2 (𝜑 → (𝜓𝜃))
51, 4mpd 15 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:  riotaeqimp  6780  marypha1lem  8499  wemaplem3  8613  xpwdomg  8650  wrdind  13685  wrd2ind  13686  sqrt2irr  15185  coprm  15630  oddprmdvds  15814  symggen  18097  efgredlemd  18364  efgredlem  18367  efgred  18368  chcoeffeq  20911  nmoleub2lem3  23134  iscmet3  23310  axtgcgrid  25583  axtg5seg  25585  axtgbtwnid  25586  wlk1walk  26770  umgr2wlk  27096  frgrnbnb  27475  friendshipgt3  27597  archiexdiv  30084  unelsiga  30537  sibfof  30742  bnj1145  31399  derangenlem  31491  l1cvpat  34863  llnexchb2  35678  hdmapglem7  37739  eel11111  39475  dmrelrnrel  39936  climrec  40350  lptre2pt  40387  0ellimcdiv  40396  iccpartlt  41885
  Copyright terms: Public domain W3C validator