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

Theorem mp2 9
Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994.)
Hypotheses
Ref Expression
mp2.1 𝜑
mp2.2 𝜓
mp2.3 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mp2 𝜒

Proof of Theorem mp2
StepHypRef Expression
1 mp2.2 . 2 𝜓
2 mp2.1 . . 3 𝜑
3 mp2.3 . . 3 (𝜑 → (𝜓𝜒))
42, 3ax-mp 5 . 2 (𝜓𝜒)
51, 4ax-mp 5 1 𝜒
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  199  imbi12i  340  pm3.2i  471  minimp-sylsimp  1559  minimp-ax2c  1561  minimp-ax2  1562  minimp-pm2.43  1563  sbcom2  2443  sstri  3604  0disj  4636  disjx0  4638  relres  5414  cnvdif  5527  difxp  5546  funopab4  5913  fun0  5942  fvsn  6431  omsinds  7069  reltpos  7342  tpostpos  7357  tpos0  7367  oaabs2  7710  swoer  7757  xpider  7803  erinxp  7806  sbthcl  8067  php  8129  elirrv  8489  inf0  8503  unctb  9012  fin1a2lem12  9218  axcc2lem  9243  axcclem  9264  brdom3  9335  brdom5  9336  brdom4  9337  pwcfsdom  9390  smobeth  9393  fpwwe2lem8  9444  fpwwe2lem9  9445  fpwwe2lem12  9448  pwxpndom2  9472  pwcdandom  9474  gchac  9488  wunex3  9548  inar1  9582  gruina  9625  ltsopi  9695  recmulnq  9771  prcdnq  9800  ltrel  10085  lerel  10087  suprfinzcl  11477  cnexALT  11813  dfle2  11965  dflt2  11966  uzrdg0i  12741  ltwefz  12745  fzennn  12750  faclbnd4lem1  13063  hashsslei  13196  0csh0  13520  isercolllem1  14376  zsum  14430  sum0  14433  znnen  14922  qnnen  14923  rpnnen  14937  ruc  14953  nthruc  14962  nthruz  14963  phicl2  15454  pwsle  16133  xpsc0  16201  xpsc1  16202  relfull  16549  relfth  16550  gicer  17699  gicerOLD  17700  oppglsm  18038  efgrelexlemb  18144  isunit  18638  opsrtoslem2  19466  xrsnsgrp  19763  pjpm  20033  1stcfb  21229  2ndc1stc  21235  2ndcctbss  21239  2ndcdisj2  21241  2ndcsep  21243  hmpher  21568  met1stc  22307  re2ndc  22585  iccpnfhmeo  22725  xrhmeo  22726  xrcmp  22728  xrconn  22729  dyadmbl  23349  opnmblALT  23352  vitalilem2  23359  vitalilem3  23360  vitali  23363  mbfimaopnlem  23403  mbfsup  23412  dgrval  23965  dgrcl  23970  dgrub  23971  dgrlb  23973  aannenlem3  24066  dvrelog  24364  logcn  24374  logccv  24390  logblog  24511  ppiub  24910  lgsquadlem1  25086  lgsquadlem2  25087  dirith2  25198  usgrexmpldifpr  26131  usgrexmplef  26132  disjxwwlksn  26780  disjxwwlkn  26789  nvrel  27427  phrel  27640  bnrel  27693  hlrel  27716  pjnormi  28550  lnopunilem1  28839  lnophmlem1  28845  xrge0infssd  29500  infxrge0lb  29503  infxrge0glb  29504  infxrge0gelb  29505  ssnnssfz  29523  xrge0iifiso  29955  omsf  30332  oms0  30333  omssubaddlem  30335  omssubadd  30336  oddpwdc  30390  rpsqrtcn  30645  bnj1023  30825  bnj1109  30831  erdszelem4  31150  erdszelem8  31154  supfz  31588  inffz  31589  inffzOLD  31590  elrn3  31628  trer  32285  fneer  32323  naim1i  32361  naim2i  32362  mont  32383  onpsstopbas  32404  bj-mp2c  32506  bj-mp2d  32507  bj-currypeirce  32519  wl-equsal1i  33300  wl-sbcom2d  33315  poimirlem25  33405  poimirlem26  33406  mblfinlem1  33417  incsequz2  33516  cncfres  33535  heiborlem3  33583  diclspsn  36302  dih1dimatlem  36437  rencldnfilem  37203  pellexlem4  37215  pellexlem5  37216  ttac  37422  idomsubgmo  37595  areaquad  37621  frege102  38079  lhe4.4ex1a  38348  eel0001  38765  eel0000  38766  eel00001  38768  eel00000  38769  e000  38814  e00  38815  fzisoeu  39327  resincncf  39851  fmtnoinf  41213  ssnn0ssfz  41892  zlmodzxzldeplem  42052
  Copyright terms: Public domain W3C validator