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  7414  marypha1lem  9473  wemaplem3  9588  xpwdomg  9625  pwfseqlem4  10702  wrdind  14760  wrd2ind  14761  sqrt2irr  16285  coprm  16748  oddprmdvds  16941  cyccom  19221  symggen  19488  efgredlemd  19762  efgredlem  19765  efgred  19766  chcoeffeq  22892  nmoleub2lem3  25148  iscmet3  25327  mulsproplem1  28142  axtgcgrid  28471  axtg5seg  28473  axtgbtwnid  28474  wlk1walk  29657  umgr2wlk  29969  frgrnbnb  30312  friendshipgt3  30417  ismntd  32974  archiexdiv  33197  fedgmullem2  33681  unelsiga  34135  sibfof  34342  bnj1145  35007  derangenlem  35176  irrdiff  37327  l1cvpat  39055  llnexchb2  39871  hdmapglem7  41931  eel11111  44743  dmrelrnrel  45231  climrec  45618  lptre2pt  45655  0ellimcdiv  45664  iccpartlt  47411  cycl3grtri  47914
  Copyright terms: Public domain W3C validator