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

Theorem mp2d 46
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 42 . 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:  marypha1lem  8196  wemaplem3  8310  xpwdomg  8347  wrdind  13271  wrd2ind  13272  sqrt2irr  14760  coprm  15204  oddprmdvds  15388  symggen  17656  efgredlemd  17923  efgredlem  17926  efgred  17927  chcoeffeq  20449  nmoleub2lem3  22651  iscmet3  22814  axtgcgrid  25076  axtg5seg  25078  axtgbtwnid  25079  frgranbnb  26310  vdgfrgragt2  26317  friendshipgt3  26411  archiexdiv  28878  unelsiga  29327  sibfof  29532  bnj1145  30118  derangenlem  30210  l1cvpat  33159  llnexchb2  33973  hdmapglem7  36039  eel11111  37771  climrec  38471  lptre2pt  38508  0ellimcdiv  38517  iccpartlt  39764  riotaeqimp  40162  1wlk1walk  40842  umgr2wlk  41155  frgrnbnb  41462  av-friendshipgt3  41551
  Copyright terms: Public domain W3C validator