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

Theorem mp2d 45
Description: A double modus ponens deduction. (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 41 . 2
51, 4mpd 15 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  marypha1lem  7913  wemaplem3  7994  xpwdomg  8032  wrdind  12702  wrd2ind  12703  sqrt2irr  13982  coprm  14241  symggen  16495  efgredlemd  16762  efgredlem  16765  efgred  16766  chcoeffeq  19387  nmoleub2lem3  21598  iscmet3  21732  axtgcgrid  23860  axtg5seg  23862  axtgbtwnid  23863  frgranbnb  25020  vdgfrgragt2  25027  friendshipgt3  25121  archiexdiv  27734  unelsiga  28134  sibfof  28282  derangenlem  28615  climrec  31609  lptre2pt  31646  0ellimcdiv  31655  eel11111  33520  bnj1145  34049  l1cvpat  34779  llnexchb2  35593  hdmapglem7  37659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator