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  7115  marypha1lem  8873  wemaplem3  8988  xpwdomg  9025  wrdind  14062  wrd2ind  14063  sqrt2irr  15580  coprm  16031  oddprmdvds  16215  cyccom  18322  symggen  18574  efgredlemd  18846  efgredlem  18849  efgred  18850  chcoeffeq  21467  nmoleub2lem3  23696  iscmet3  23873  axtgcgrid  26233  axtg5seg  26235  axtgbtwnid  26236  wlk1walk  27404  umgr2wlk  27711  frgrnbnb  28054  friendshipgt3  28159  ismntd  30650  archiexdiv  30824  fedgmullem2  31034  unelsiga  31398  sibfof  31603  bnj1145  32270  derangenlem  32423  l1cvpat  36223  llnexchb2  37038  hdmapglem7  39098  eel11111  41199  dmrelrnrel  41631  climrec  42023  lptre2pt  42060  0ellimcdiv  42069  iccpartlt  43719
  Copyright terms: Public domain W3C validator