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

Theorem mp2 9
Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
mp2.1  |-  ph
mp2.2  |-  ps
mp2.3  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mp2  |-  ch

Proof of Theorem mp2
StepHypRef Expression
1 mp2.2 . 2  |-  ps
2 mp2.1 . . 3  |-  ph
3 mp2.3 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3ax-mp 5 . 2  |-  ( ps 
->  ch )
51, 4ax-mp 5 1  |-  ch
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5
This theorem is referenced by:  impbii  188  imbi12i  324  pm3.2i  453  sbcom2  2193  sstri  3426  0disj  4360  disjx0  4362  relres  5213  cnvdif  5322  difxp  5341  funopab4  5531  fun0  5553  fvsn  6006  reltpos  6878  tpostpos  6893  tpos0  6903  oaabs2  7212  swoer  7257  xpider  7300  erinxp  7303  sbthcl  7558  php  7620  inf0  7952  unctb  8498  fin1a2lem12  8704  axcc2lem  8729  axcclem  8750  brdom3  8819  brdom5  8820  brdom4  8821  pwcfsdom  8871  smobeth  8874  fpwwe2lem8  8926  fpwwe2lem9  8927  fpwwe2lem12  8930  pwxpndom2  8954  pwcdandom  8956  gchac  8970  wunex3  9030  inar1  9064  gruina  9107  ltsopi  9177  recmulnq  9253  prcdnq  9282  ltrel  9560  lerel  9562  suprfinzcl  10894  cnexALT  11135  dfle2  11274  dflt2  11275  uzrdg0i  11973  ltwefz  11977  fzennn  11981  faclbnd4lem1  12273  hashsslei  12388  0csh0  12675  isercolllem1  13489  zsum  13542  sum0  13545  znnen  13948  qnnen  13949  rpnnen  13962  ruc  13978  nthruc  13986  nthruz  13987  phicl2  14300  pwsle  14899  xpsc0  14967  xpsc1  14968  relfull  15314  relfth  15315  gicer  16441  oppglsm  16779  efgrelexlemb  16885  isunit  17419  opsrtoslem2  18262  xrsnsgrp  18567  pjpm  18830  1stcfb  20031  2ndc1stc  20037  2ndcctbss  20041  2ndcdisj2  20043  2ndcsep  20045  hmpher  20370  met1stc  21109  re2ndc  21391  iccpnfhmeo  21530  xrhmeo  21531  xrcmp  21533  xrcon  21534  dyadmbl  22094  opnmblALT  22097  vitalilem2  22103  vitalilem3  22104  vitali  22107  mbfimaopnlem  22147  mbfsup  22156  dgrval  22710  dgrcl  22715  dgrub  22716  dgrlb  22718  aannenlem3  22811  dvrelog  23105  logcn  23115  logccv  23131  logblog  23250  ppiub  23596  lgsquadlem1  23746  lgsquadlem2  23747  dirith2  23830  usgraexmpldifpr  24521  usgraexmpl  24522  disjxwwlks  24857  disjxwwlkn  24866  konigsberg  25108  nvrel  25612  phrel  25847  bnrel  25900  hlrel  25923  pjnormi  26756  lnopunilem1  27045  lnophmlem1  27051  xrge0infssd  27731  ssnnssfz  27750  xrge0iifiso  28071  omsf  28423  oms0  28424  omssubaddlem  28426  omssubadd  28427  oddpwdc  28476  erdszelem4  28827  erdszelem8  28831  supfz  29273  inffz  29274  elrn3  29358  omsinds  29464  naim1i  30005  naim2i  30006  mont  30027  onpsstopbas  30048  wl-equsal1i  30161  wl-sbcom2d  30176  mblfinlem1  30216  trer  30300  fneer  30337  incsequz2  30408  cncfres  30427  heiborlem3  30475  rencldnfilem  30919  pellexlem4  30933  pellexlem5  30934  ttac  31144  idomsubgmo  31323  areaquad  31352  lhe4.4ex1a  31402  fzisoeu  31666  resincncf  31843  ssnn0ssfz  33138  zlmodzxzldeplem  33299  eel0001  33855  eel0000  33856  eel00001  33858  eel00000  33859  e000  33904  e00  33905  bnj1023  34186  bnj1109  34192  bj-mp2c  34476  bj-mp2d  34477  bj-alrimih  34556  diclspsn  37334  dih1dimatlem  37469  frege102  38464
  Copyright terms: Public domain W3C validator