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  211  imbi12i  353  pm3.2i  473  minimp-syllsimp  1619  minimp-ax2c  1621  minimp-ax2  1622  minimp-pm2.43  1623  darii  2748  barbarilem  2751  festino  2757  baroco  2759  darapti  2767  sstri  3975  0disj  5057  disjx0  5059  opthhausdorff  5406  relres  5881  cnvdif  6001  difxp  6020  funopab4  6391  fun0  6418  omsinds  7599  reltpos  7896  tpos0  7921  oaabs2  8271  swoer  8318  xpider  8367  sbthcl  8638  php  8700  elirrv  9059  inf0  9083  unctb  9626  fin1a2lem12  9832  axcc2lem  9857  axcclem  9878  brdom3  9949  brdom5  9950  brdom4  9951  pwcfsdom  10004  smobeth  10007  pwxpndom2  10086  pwdjundom  10088  gchac  10102  wunex3  10162  inar1  10196  gruina  10239  ltsopi  10309  recmulnq  10385  prcdnq  10414  ltrel  10702  lerel  10704  suprfinzcl  12096  cnexALT  12384  dfle2  12539  dflt2  12540  uzrdg0i  13326  ltwefz  13330  fzennn  13335  faclbnd4lem1  13652  hashsslei  13786  0csh0  14154  isercolllem1  15020  zsum  15074  sum0  15077  znnen  15564  qnnen  15565  rpnnen  15579  ruc  15595  nthruc  15604  nthruz  15605  phicl2  16104  relfull  17177  relfth  17178  gicer  18415  oppglsm  18766  efgrelexlemb  18875  isunit  19406  xrsnsgrp  20580  pjpm  20851  1stcfb  22052  2ndc1stc  22058  2ndcctbss  22062  2ndcdisj2  22064  2ndcsep  22066  hmpher  22391  met1stc  23130  re2ndc  23408  iccpnfhmeo  23548  xrhmeo  23549  xrcmp  23551  xrconn  23552  dyadmbl  24200  opnmblALT  24203  vitalilem2  24209  vitalilem3  24210  vitali  24213  mbfimaopnlem  24255  mbfsup  24264  dgrval  24817  dgrcl  24822  dgrub  24823  dgrlb  24825  aannenlem3  24918  dvrelog  25219  logcn  25229  logccv  25245  ppiub  25779  lgsquadlem1  25955  lgsquadlem2  25956  addsqrexnreu  26017  addsqnreup  26018  2sqreunnlem2  26030  dirith2  26103  usgrexmpldifpr  27039  usgrexmplef  27040  disjxwwlksn  27681  disjxwwlkn  27691  nvrel  28378  phrel  28591  bnrel  28643  hlrel  28666  pjnormi  29497  lnopunilem1  29786  lnophmlem1  29792  xrge0infssd  30484  infxrge0lb  30487  infxrge0glb  30488  infxrge0gelb  30489  ssnnssfz  30509  xrge0iifiso  31178  omsf  31554  oms0  31555  omssubaddlem  31557  omssubadd  31558  oddpwdc  31612  rpsqrtcn  31864  bnj1023  32052  bnj1109  32058  erdszelem4  32441  erdszelem8  32445  gonan0  32639  supfz  32960  inffz  32961  trer  33664  fneer  33701  naim1i  33739  naim2i  33740  nmotru  33756  onpsstopbas  33778  bj-mp2c  33879  bj-mp2d  33880  bj-bijust00  33910  bj-cbvalim  33978  bj-cbvexim  33979  bj-cbvalimi  33980  bj-cbveximi  33981  pibt2  34697  wl-equsal1i  34782  wl-sbcom2d  34796  poimirlem25  34916  poimirlem26  34917  mblfinlem1  34928  incsequz2  35023  cncfres  35042  heiborlem3  35090  diclspsn  38329  dih1dimatlem  38464  rencldnfilem  39417  pellexlem4  39429  pellexlem5  39430  ttac  39633  idomsubgmo  39798  areaquad  39823  frege102  40311  lhe4.4ex1a  40661  eel0000  41054  eel00001  41055  eel00000  41056  e000  41101  e00  41102  fzisoeu  41567  resincncf  42158  aiota0def  43295  fvmptrabdm  43493  fmtnoinf  43699  ssnn0ssfz  44398  zlmodzxzldeplem  44554
  Copyright terms: Public domain W3C validator