Axiom ax-mp 5

Description: Rule of Modus Ponens. The postulated inference rule of propositional calculus. See e.g. Rule 1 of [Hamilton] p. 73. The rule says, "if ph is true, and ph implies ps, then ps must also be true." This rule is sometimes called "detachment", since it detaches the minor premise from the major premise. "Modus ponens" is short for "modus ponendo ponens", a Latin phrase that means "the mode that by affirming affirms" - remark in [Sanford] p. 39. This rule is similar to the rule of modus tollens mto 651.

Note: In some web page displays such as the Statement List, the symbols "& " and "=> " informally indicate the relationship between the hypotheses and the assertion (conclusion), abbreviating the English words "and" and "implies." They are not part of the formal language. (Contributed by NM, 30-Sep-1992.)

Hypotheses

Ref	Expression
min	|- ph
maj	|- ( ph -> ps )

Assertion

Ref	Expression
ax-mp	|- ps

Detailed syntax breakdown of Axiom ax-mp

Step	Hyp	Ref	Expression
1		wps	1 wff ps

This axiom is referenced by:  mp2b  8  a1i  9  mp1i  10  a2i  11  mpd  13  mp2  16  idALT  20  simpli  110  simpri  112  biimpi  119  bicomi  131  mpbi  144  mpbir  145  imbi1i  237  a1bi  242  tbt  246  biantru  300  biantrur  301  mp2an  422  pm2.65i  628  notnoti  634  pm2.21i  635  pm2.24ii  636  notbii  657  nbn  688  ori  712  orci  720  olci  721  biorfi  735  imorri  738  dcbii  825  simp1i  990  simp2i  991  simp3i  992  3mix1i  1153  3mix2i  1154  3mix3i  1155  3jaoi  1281  mptru  1340  dfnot  1349  mptnan  1401  mtpor  1403  mtpxor  1404  mpg  1427  19.23h  1474  hbequid  1493  axi12  1494  nfri  1499  spi  1516  19.21  1562  eximii  1581  19.35i  1604  nfn  1636  19.37aiv  1653  19.23  1656  exan  1671  equid  1677  hbae  1696  equvini  1731  equveli  1732  sbid  1747  sbieh  1763  exdistrfor  1772  dveeq2or  1788  ax11v  1799  ax11ev  1800  equs5or  1802  sb4or  1805  sb4bor  1807  nfsb2or  1809  sbequilem  1810  sbequi  1811  speiv  1834  nfsbxy  1915  nfsbxyt  1916  sbco  1941  sbcocom  1943  sbcomxyyz  1945  elsb3  1951  elsb4  1952  sbal1yz  1976  dvelimALT  1985  dvelimfv  1986  dvelimor  1993  eumoi  2032  moani  2069  eqeq1i  2147  eqeq2i  2150  eleq1i  2205  eleq2i  2206  nfcrii  2274  neeq1i  2323  neeq2i  2324  necon3i  2356  rspec  2484  rgen2a  2486  mprg  2489  r19.21  2508  r19.23  2540  raleqi  2630  rexeqi  2631  rabeqif  2677  elv  2690  elexi  2698  ceqsal  2715  vtocl3  2742  vtoclef  2759  vtocle  2760  spcv  2779  spcev  2780  clel3  2820  elabf  2827  elab2  2832  elab3  2836  euxfrdc  2870  reueq  2883  rmoimi2  2887  sbsbc  2913  sbc8g  2916  sbc6  2934  sbcie  2943  sbcrex  2988  csbvarg  3030  csbief  3044  csbie2  3049  sbnfc2  3060  sseli  3093  sselii  3094  sseq1i  3123  sseq2i  3124  difeq1i  3190  difeq2i  3191  uneq1i  3226  uneq2i  3227  ineq1i  3273  ineq2i  3274  ssinss1  3305  difdif2ss  3333  n0ii  3371  ne0ii  3372  vn0  3373  vn0m  3374  abf  3406  disj2  3418  difid  3431  0dif  3434  disjdif  3435  difin0  3436  undif1ss  3437  difdifdirss  3447  rgenm  3465  iftruei  3480  iffalsei  3483  ifbieq2i  3495  ifbieq12i  3497  pweqi  3514  pwid  3525  sneqi  3539  elsn  3543  elpr  3548  elsn2  3559  ralsn  3567  rexsn  3568  eltp  3571  rabrsndc  3591  preq1i  3603  preq2i  3604  prid1  3629  snnz  3642  snm  3643  prnz  3645  prm  3646  tpnz  3648  snsssn  3688  opeq1i  3708  opeq2i  3709  unieqi  3746  unissi  3759  inteqi  3775  intmin2  3797  intab  3800  intsn  3806  iinconstm  3822  iuniin  3823  iinss1  3825  iunxdif2  3861  ssiinf  3862  iinss  3864  iinss2  3865  iinab  3874  iundif2ss  3878  iindif2m  3880  iinin2m  3881  iunxsn  3889  iunxprg  3893  iinpw  3903  sndisj  3925  disjxsn  3927  breqi  3935  breq1i  3936  breq2i  3937  brab1  3975  opabbii  3995  truni  4040  bm1.3ii  4049  a9evsep  4050  ax9vsep  4051  zfnuleu  4052  axnul  4053  ssexi  4066  rabex  4072  elpw2  4082  pwnss  4083  iin0r  4093  intv  4094  pwex  4107  snex  4109  notnotsnex  4111  ord3ex  4114  dtruarb  4115  undifexmid  4117  intid  4146  opnzi  4157  copsexg  4166  opelopabf  4196  epelc  4213  elon  4296  inton  4315  onn0  4322  onm  4323  elsuc  4328  elsuc2  4329  sucid  4339  iunsuc  4342  onordi  4348  ontrci  4349  onelssi  4351  eusvnf  4374  ssonunii  4405  sucex  4415  onssi  4431  onsuci  4432  ordtriexmidlem  4435  ordtriexmidlem2  4436  ordtriexmid  4437  ordtri2orexmid  4438  2ordpr  4439  ontr2exmid  4440  onsucsssucexmid  4442  onsucelsucexmid  4445  regexmidlemm  4447  reg2exmid  4451  onirri  4458  ruALT  4466  onprc  4467  sucon  4468  dtru  4475  0elsucexmid  4480  ordpwsucexmid  4485  ordtri2or2exmid  4486  dcextest  4495  omex  4507  find  4513  omelon  4522  nnoni  4524  limom  4527  nnregexmid  4534  omsinds  4535  xpeq1i  4559  xpeq2i  4560  0nelxp  4567  opthprc  4590  mosubop  4605  releqi  4622  relssi  4630  relin1  4657  relin2  4658  reldif  4659  inopab  4671  difopab  4672  xpiindim  4676  opabbi2dv  4688  ideq  4691  coeq1i  4698  coeq2i  4699  cnveqi  4714  eldm  4736  eldm2  4737  dmeqi  4740  dmv  4755  rneqi  4767  elrnmpti  4792  dmex  4805  rnex  4806  reseq1i  4815  reseq2i  4816  residm  4851  resex  4860  resmpt3  4868  imaeq1i  4878  imaeq2i  4879  elima  4886  imaex  4894  elimasn  4906  args  4908  epini  4910  dfse2  4912  relbrcnv  4919  cotr  4920  issref  4921  cnvsym  4922  asymref  4924  intirr  4925  codir  4927  qfto  4928  ssrnres  4981  cnveq0  4995  cnvsn0  5007  dmsnop  5012  rnsnop  5019  resdm2  5029  dfco2a  5039  cocnvcnv1  5049  coi2  5055  coires1  5056  cnvssrndm  5060  cossxp  5061  cocnvres  5063  relrelss  5065  relcoi2  5069  unidmrn  5071  dfdm2  5073  unixpm  5074  cnvexg  5076  cnvex  5077  cnviinm  5080  iotaval  5099  funeqi  5144  funi  5155  funres  5164  funcnvsn  5168  funcnvcnv  5182  funin  5194  funcnvres  5196  isarep2  5210  fneq1i  5217  fneq2i  5218  fnresdisj  5233  fnresi  5240  mpt0  5250  dmmpti  5252  feq1i  5265  feq2i  5266  fdmi  5280  fun2  5296  fssres  5298  resasplitss  5302  fintm  5308  fconst6  5322  f1ores  5382  foimacnv  5385  resdif  5389  funcocnv2  5392  f1ovi  5406  fveq1i  5422  fveq2i  5424  0fv  5456  fvun1  5487  fvopab3ig  5495  fvmptss2  5496  mptrcl  5503  elfvmptrab1  5515  fndmdif  5525  fneqeql2  5529  f1oresrab  5585  fmptco  5586  fnressn  5606  fressnfv  5607  fmptap  5610  fvsnun1  5617  fvsnun2  5618  fsnunfv  5621  fconst2  5637  mptex  5646  riotabiia  5747  acexmidlema  5765  acexmidlemb  5766  acexmidlemcase  5769  acexmidlem2  5771  acexmidlemv  5772  oveq1i  5784  oveq2i  5785  oveqi  5787  oprabidlem  5802  0neqopab  5816  oprabbii  5826  oprabss  5857  mpompt  5863  funoprab  5871  fnoprab  5874  fovcl  5876  ovigg  5891  elmpocl  5968  resfunexgALT  6008  cofunexg  6009  opabex3d  6019  opabex3  6020  1st0  6042  2nd0  6043  op1st  6044  op2nd  6045  f1stres  6057  f2ndres  6058  fo1stresm  6059  fo2ndresm  6060  1stcof  6061  2ndcof  6062  1stexg  6065  2ndexg  6066  releldm2  6083  reldm  6084  dfoprab3  6089  mpomptsx  6095  mpompts  6096  fnmpoi  6102  dmmpo  6103  mpoexxg  6108  1stconst  6118  2ndconst  6119  dfmpo  6120  algrflem  6126  algrflemg  6127  cnvoprab  6131  f1od2  6132  mpoxopn0yelv  6136  mpoxopoveq  6137  tposssxp  6146  brtpos2  6148  reldmtpos  6150  dftpos2  6158  dftpos4  6160  tpostpos  6161  tpostpos2  6162  tposfo  6168  tposf  6169  tposeqi  6174  tposex  6175  tposoprab  6177  issmo  6185  smores  6189  smores2  6191  iordsmo  6194  smo0  6195  tfrlem8  6215  tfrexlem  6231  tfr1onlem3  6235  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlemres  6246  tfri1dALT  6248  tfri2  6263  rdgisuc1  6281  rdg0  6284  frecfun  6292  frec0g  6294  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecrdg  6305  2on0  6323  xp01disj  6330  2oconcl  6336  fnoa  6343  oaexg  6344  fnom  6346  omexg  6347  fnoei  6348  oeiexg  6349  oei0  6355  oacl  6356  oasuc  6360  o1p1e2  6364  omsuc  6368  nna0r  6374  nnm0r  6375  1onn  6416  2onn  6417  3onn  6418  4onn  6419  eqerlem  6460  elqs  6480  qsex  6486  ecqs  6491  iinerm  6501  th3qlem1  6531  th3q  6534  mapsn  6584  mapsnf1o3  6591  ixpiinm  6618  ixpssmap  6626  brdom  6644  f1dom  6654  enref  6659  dom2  6669  idssen  6671  ssdomg  6672  ensymi  6676  ensn1  6690  fiprc  6709  1domsn  6713  xpcomf1o  6719  xpcomco  6720  dom0  6732  0dom  6733  xpmapenlem  6743  phplem2  6747  php5  6752  snnen2og  6753  1nen2  6755  php5dom  6757  ssfilem  6769  ssfiexmid  6770  domfiexmid  6772  0fin  6778  diffitest  6781  findcard  6782  findcard2  6783  findcard2s  6784  isinfinf  6791  ac6sfi  6792  inffiexmid  6800  unfiexmid  6806  xpfi  6818  fisseneq  6820  ssfirab  6822  en1eqsn  6836  snexxph  6838  sbthlem2  6846  sbthlemi3  6847  sbthlemi6  6850  sbthlem7  6851  fi0  6863  supeq1i  6875  infeq1i  6900  djuexb  6929  djuf1olemr  6939  inresflem  6945  djuinr  6948  updjudhcoinlf  6965  updjudhcoinrg  6966  casefun  6970  caserel  6972  caseinj  6974  caseinl  6976  caseinr  6977  omp1eomlem  6979  endjusym  6981  difinfsn  6985  difinfinf  6986  djuinj  6991  0ct  6992  ctmlemr  6993  ctssdclemn0  6995  ctssdccl  6996  omct  7002  ctfoex  7003  finomni  7012  exmidomni  7014  fodjuomni  7021  nnnninf  7023  ctssexmid  7024  fodjumkv  7034  card0  7044  exmidonfinlem  7049  dju1p1e2  7053  exmidfodomrlemim  7057  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  0npi  7121  dmaddpi  7133  dmmulpi  7134  1lt2pi  7148  0nnq  7172  1nq  7174  dmaddpq  7187  dmmulpq  7188  rec1nq  7203  1lt2nq  7214  halfnqq  7218  prarloclemarch2  7227  enq0enq  7239  nqnq0pi  7246  nnnq0lem1  7254  addnnnq0  7257  mulnnnq0  7258  nq0m0r  7264  addpinq1  7272  prarloclem5  7308  prarloclemcalc  7310  1pr  7362  1idprl  7398  1idpru  7399  ltexprlemm  7408  recexprlem1ssl  7441  recexprlem1ssu  7442  suplocexprlemell  7521  suplocexprlem2b  7522  suplocexprlemmu  7526  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemub  7531  suplocexprlemlub  7532  prsrlem1  7550  addsrpr  7553  mulsrpr  7554  gt0srpr  7556  0nsr  7557  0r  7558  1sr  7559  m1r  7560  m1m1sr  7569  caucvgsr  7610  suplocsrlempr  7615  addresr  7645  mulresr  7646  pitonnlem1  7653  peano1nnnn  7660  axi2m1  7683  axcnre  7689  peano5nnnn  7700  axcaucvg  7708  mulid1i  7768  mulid2i  7769  pnfnre  7807  mnfnre  7808  pnfnemnf  7820  mnfxr  7822  rexri  7823  ltnri  7856  ltleii  7866  00id  7903  addid1i  7904  addid2i  7905  0cnALT  7952  negeqi  7956  negicn  7963  neg0  8008  renegcli  8024  negcli  8030  negidi  8031  negnegi  8032  subidi  8033  subid1i  8034  negne0bi  8035  negrebi  8036  mul02i  8152  mul01i  8153  mulm1i  8165  leidi  8247  gt0ne0ii  8249  inelr  8346  msqge0i  8379  gt0ap0ii  8390  1div1e1  8464  div1i  8500  eqnegi  8501  recclapi  8502  recidapi  8503  divmulapi  8526  rerecclapi  8537  redivclapi  8539  recgt0  8608  ltp1i  8663  divgt0ii  8677  ltmul1ii  8686  ltdiv1ii  8687  sup3exmid  8715  peano5nni  8723  nnrei  8729  1nn  8731  nngt0i  8750  neg1ap0  8829  2timesi  8850  times2i  8851  2nn  8881  3nn  8882  4nn  8883  5nn  8884  6nn  8885  7nn  8886  8nn  8887  9nn  8888  2muline0  8945  rehalfcli  8968  nn0ssre  8981  nnnn0i  8985  dfn2  8990  0nn0  8992  nn0ge0i  9004  zrei  9060  neg1z  9086  nn0negzi  9089  dfz2  9123  nneoi  9155  peano5uzi  9160  dfuzi  9161  nn0ind-raph  9168  deceq1i  9188  deceq2i  9189  10nn  9197  numltc  9207  eluzel2  9331  eluz1i  9333  nn0uz  9360  nnuz  9361  infrenegsupex  9389  lbzbi  9408  divfnzn  9413  qdivcl  9435  irrmul  9439  cnref1o  9440  0ltpnf  9568  mnflt0  9570  0lepnf  9576  xrltnsym  9579  xrlttri3  9583  nltpnft  9597  ngtmnft  9600  xrrebnd  9602  xnegmnf  9612  xneg0  9614  xltnegi  9618  xaddmnf1  9631  xaddmnf2  9632  mnfaddpnf  9634  xaddid1  9645  xnn0lenn0nn0  9648  xnn0xadd0  9650  xposdif  9665  ixxex  9682  iooval2  9698  unirnioo  9756  ioorebasg  9758  elrege0  9759  fzval2  9793  fzen  9823  fzprval  9862  fztpval  9863  uzdisj  9873  ige2m1fz  9890  fz01or  9891  fz1ssfz0  9897  fz0tp  9901  nn0disj  9915  1fv  9916  4fvwrd4  9917  fzo0ss1  9951  fzo01  9993  fzo12sn  9994  fzo0to2pr  9995  fzo0to3tp  9996  fzo0to42pr  9997  qbtwnxr  10035  flval  10045  modqfrac  10110  modqmulnn  10115  q2txmodxeq0  10157  frecuzrdgdom  10191  frecuzrdgfun  10193  frecuzrdgsuct  10197  frechashgf1o  10201  nnct  10208  fxnn0nninf  10211  0tonninf  10212  1tonninf  10213  iseqvalcbv  10230  ser0f  10288  0exp0e1  10298  qexpcl  10309  qexpclz  10314  m1expcl2  10315  1exp  10322  sqvali  10372  sqcli  10373  sqeq0i  10374  resqcli  10377  sq1  10386  neg1sqe1  10387  iexpcyc  10397  facnn  10473  fac0  10474  fac1  10475  fac2  10477  fac3  10478  fac4  10479  bcval  10495  bcm1k  10506  bcpasc  10512  bccl  10513  4bc3eq4  10519  4bc2eq6  10520  hashinfom  10524  hashennn  10526  hashfz1  10529  fihasheq0  10540  hash0  10543  hashsng  10544  fihashen1  10545  omgadd  10548  hashp1i  10556  hashxp  10572  fimaxq  10573  zfz1iso  10584  shftidt2  10604  cjexp  10665  re0  10667  im0  10668  re1  10669  im1  10670  cj0  10673  cji  10674  recli  10683  imcli  10684  cjcli  10685  replimi  10686  cjcji  10687  reim0bi  10688  rerebi  10689  cjrebi  10690  recji  10691  imcji  10692  cjmulrcli  10693  cjmulvali  10694  cjmulge0i  10695  renegi  10696  imnegi  10697  cjnegi  10698  addcji  10699  uzin2  10759  rexanuz  10760  rexfiuz  10761  sqrtrval  10772  sqrt0  10776  resqrexlemcalc3  10788  resqrexlemcvg  10791  resqrex  10798  abs0  10830  absi  10831  qabsor  10847  absimle  10856  recan  10881  caubnd2  10889  leabsi  10900  absrei  10901  sqrtpclii  10902  sqrtgt0ii  10903  absvalsqi  10912  absvalsq2i  10913  abscli  10914  absge0i  10915  absval2i  10916  abs00i  10917  absgt0api  10918  absnegi  10919  abscji  10920  releabsi  10921  infxrnegsupex  11032  xrbdtri  11045  cbvsum  11129  sumeq1i  11132  sum0  11157  isumz  11158  fisumss  11161  fsumsersdc  11164  fsumadd  11175  isumclim  11190  isumclim3  11192  fsumcnv  11206  modfsummodlem1  11225  fsumrelem  11240  binomlem  11252  binom  11253  arisum2  11268  expcnv  11273  0.999...  11290  prodf1f  11312  cbvprod  11327  prodeq1i  11330  ef0lem  11366  esum  11368  ere  11376  ege2le3  11377  ef0  11378  eff2  11386  efsep  11397  reeff1  11407  sin0  11436  cos0  11437  ef01bndlem  11463  cos2bnd  11467  sincos1sgn  11471  sincos2sgn  11472  sin4lt0  11473  eirr  11485  0dvds  11513  dvds1  11551  z0even  11608  n2dvdsm1  11610  z2even  11611  n2dvds3  11612  ndvdssub  11627  ndvdsi  11630  flodddiv4  11631  gcddvds  11652  gcd1  11675  6gcd4e2  11683  bezoutlembi  11693  dfgcd3  11698  dfgcd2  11702  lcmval  11744  lcmcllem  11748  lcmledvds  11751  3lcm2e6woprm  11767  qredeu  11778  isprm2lem  11797  isprm3  11799  prm2orodd  11807  sqrt2irr0  11842  pw2dvds  11844  phicl2  11890  phi1  11895  dfphi2  11896  phiprmpw  11898  ennnfonelemp1  11919  ennnfonelem1  11920  ennnfonelemkh  11925  ennnfonelemex  11927  ennnfonelemnn0  11935  ennnfonelemr  11936  exmidunben  11939  ctinfomlemom  11940  ctinfom  11941  ctinf  11943  qnnen  11944  structcnvcnv  11975  structfun  11977  structfn  11978  ndxarg  11982  ndxid  11983  setsresg  11997  setsslnid  12010  strleun  12048  strle1g  12049  istopon  12180  topontopi  12183  toponunii  12184  toponrestid  12188  istps  12199  topontopn  12204  eltpsi  12208  eltg4i  12224  eltg3  12226  tg1  12228  tg2  12229  tgclb  12234  topnex  12255  sn0topon  12257  distps  12260  cldrcl  12271  sn0cld  12306  restco  12343  lmrcl  12360  ssidcn  12379  cnconst2  12402  cnptopresti  12407  cnptoprest  12408  txuni2  12425  txbas  12427  eltx  12428  txcnp  12440  upxp  12441  txcnmpt  12442  uptx  12443  txcn  12444  txrest  12445  txlm  12448  cnmptid  12450  cnmpt1st  12457  cnmpt2nd  12458  hmeofn  12471  psmetge0  12500  ismeti  12515  xmetunirn  12527  xmetge0  12534  unirnblps  12591  unirnbl  12592  mopnex  12674  qtopbasss  12690  retop  12693  uniretop  12694  iooretopg  12697  cnxmet  12700  cntoptopon  12701  cnbl0  12703  rexmet  12710  blssioo  12714  tgioo  12715  tgqioo  12716  cnopnap  12763  limcresi  12804  dvfvalap  12819  dvidlemap  12829  dvcnp2cntop  12832  dvcoapbr  12840  dvexp2  12845  dvrecap  12846  dveflem  12855  dvef  12856  sin0pilem1  12862  sin0pilem2  12863  pilem3  12864  pigt2lt4  12865  pire  12867  sinhalfpilem  12872  pidiv2halves  12876  cosneghalfpi  12879  cospi  12881  efipi  12882  sin2pi  12884  cos2pi  12885  ef2pi  12886  cosq14gt0  12913  coseq00topi  12916  coseq0negpitopi  12917  sincos4thpi  12921  sincos6thpi  12923  sincos3rdpi  12924  pigt3  12925  cos02pilt1  12932  ex-fl  12937  ex-ceil  12938  ex-exp  12939  ex-fac  12940  ex-gcd  12943  bj-dcdc  12965  bj-stdc  12966  bj-dcst  12967  bj-stst  12968  bj-el2oss1o  12981  elabf2  12989  bd0  13022  bdeli  13044  bdcriota  13081  bdbm1.3ii  13089  bdinex1  13097  bdssexi  13101  bj-inex  13105  bj-snex  13111  bj-sucex  13121  bj-d0clsepcl  13123  bj-omind  13132  bj-om  13135  bj-2inf  13136  bj-peano2  13137  bdpeano5  13141  bj-omssonALT  13161  bj-inf2vnlem1  13168  bj-omex2  13175  bj-nn0sucALT  13176  subctctexmid  13196  nninfall  13204  nninfsellemqall  13211  nninfsellemeqinf  13212  nninfomnilem  13214  nninfomni  13215  exmidsbthrlem  13217  sbthom  13221  isomninnlem  13225  isomninn  13226  cvgcmp2nlemabs  13227  trilpolemisumle  13231  trilpolemeq1  13233  trilpo  13236  taupi  13239