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  6599  marypha1lem  8299  wemaplem3  8413  xpwdomg  8450  wrdind  13430  wrd2ind  13431  sqrt2irr  14922  coprm  15366  oddprmdvds  15550  symggen  17830  efgredlemd  18097  efgredlem  18100  efgred  18101  chcoeffeq  20631  nmoleub2lem3  22855  iscmet3  23031  axtgcgrid  25296  axtg5seg  25298  axtgbtwnid  25299  wlk1walk  26438  umgr2wlk  26748  frgrnbnb  27055  friendshipgt3  27144  archiexdiv  29571  unelsiga  30020  sibfof  30225  bnj1145  30822  derangenlem  30914  l1cvpat  33860  llnexchb2  34674  hdmapglem7  36740  eel11111  38471  dmrelrnrel  38928  climrec  39271  lptre2pt  39308  0ellimcdiv  39317  iccpartlt  40688
  Copyright terms: Public domain W3C validator