Axiom ax-mp 7

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 𝜑 is true, and 𝜑 implies 𝜓, then 𝜓 must also be true." This rule is sometimes called "detachment," since it detaches the minor premise from the major premise.

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, 5-Aug-1993.)

Hypotheses

Ref	Expression
min	⊢ 𝜑
maj	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ax-mp	⊢ 𝜓

Detailed syntax breakdown of Axiom ax-mp

Step	Hyp	Ref	Expression
1		wps	1 wff 𝜓

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  297  biantrur  298  mp2an  418  pm2.65i  606  notnoti  612  pm2.21i  613  pm2.24ii  614  notbii  632  nbn  653  ori  680  orci  688  olci  689  biorfi  703  imorri  706  simp1i  955  simp2i  956  simp3i  957  3mix1i  1118  3mix2i  1119  3mix3i  1120  3jaoi  1246  mptru  1305  dfnot  1314  mptnan  1366  mtpor  1368  mtpxor  1369  mpg  1392  19.23h  1439  hbequid  1458  axi12  1459  nfri  1464  spi  1481  19.21  1527  eximii  1545  19.35i  1568  nfn  1600  19.37aiv  1617  19.23  1620  exan  1635  equid  1641  hbae  1660  equvini  1695  equveli  1696  sbid  1711  sbieh  1727  exdistrfor  1735  dveeq2or  1751  ax11v  1762  ax11ev  1763  equs5or  1765  sb4or  1768  sb4bor  1770  nfsb2or  1772  sbequilem  1773  sbequi  1774  speiv  1797  nfsbxy  1873  nfsbxyt  1874  sbco  1897  sbcocom  1899  sbcomxyyz  1901  elsb3  1907  elsb4  1908  sbal1yz  1932  dvelimALT  1941  dvelimfv  1942  dvelimor  1949  eumoi  1988  moani  2025  eqeq1i  2102  eqeq2i  2105  eleq1i  2160  eleq2i  2161  nfcrii  2228  neeq1i  2277  neeq2i  2278  necon3i  2310  rspec  2438  rgen2a  2440  mprg  2443  r19.21  2461  r19.23  2493  raleqi  2580  rexeqi  2581  rabeqif  2624  elv  2637  elexi  2645  ceqsal  2662  vtocl3  2689  vtoclef  2706  vtocle  2707  spcv  2726  spcev  2727  clel3  2766  elabf  2773  elab2  2777  elab3  2781  euxfrdc  2815  reueq  2828  rmoimi2  2832  sbsbc  2858  sbc8g  2861  sbc6  2879  sbcie  2887  sbcrex  2932  csbvarg  2972  csbief  2986  csbie2  2991  sbnfc2  3002  sseli  3035  sselii  3036  sseq1i  3065  sseq2i  3066  difeq1i  3129  difeq2i  3130  uneq1i  3165  uneq2i  3166  ineq1i  3212  ineq2i  3213  ssinss1  3244  difdif2ss  3272  n0ii  3310  ne0ii  3311  vn0  3312  vn0m  3313  abf  3345  disj2  3357  difid  3370  0dif  3373  disjdif  3374  difin0  3375  undif1ss  3376  difdifdirss  3386  rgenm  3404  iftruei  3419  iffalsei  3422  ifbieq2i  3434  ifbieq12i  3436  pweqi  3453  pwid  3464  sneqi  3478  elsn  3482  elpr  3487  elsn2  3498  ralsn  3506  rexsn  3507  eltp  3510  rabrsndc  3530  preq1i  3542  preq2i  3543  prid1  3568  snnz  3581  snm  3582  prnz  3584  prm  3585  tpnz  3587  snsssn  3627  opeq1i  3647  opeq2i  3648  unieqi  3685  unissi  3698  inteqi  3714  intmin2  3736  intab  3739  intsn  3745  iinconstm  3761  iuniin  3762  iinss1  3764  iunxdif2  3800  ssiinf  3801  iinss  3803  iinss2  3804  iinab  3813  iundif2ss  3817  iindif2m  3819  iinin2m  3820  iunxsn  3828  iinpw  3841  sndisj  3863  disjxsn  3865  breqi  3873  breq1i  3874  breq2i  3875  brab1  3912  opabbii  3927  truni  3972  bm1.3ii  3981  a9evsep  3982  ax9vsep  3983  zfnuleu  3984  axnul  3985  ssexi  3998  rabex  4004  elpw2  4014  pwnss  4015  iin0r  4025  intv  4026  pwex  4039  snex  4041  notnotsnex  4043  ord3ex  4046  dtruarb  4047  undifexmid  4049  intid  4075  opnzi  4086  copsexg  4095  opelopabf  4125  epelc  4142  elon  4225  inton  4244  onn0  4251  onm  4252  elsuc  4257  elsuc2  4258  sucid  4268  iunsuc  4271  onordi  4277  ontrci  4278  onelssi  4280  eusvnf  4303  ssonunii  4334  sucex  4344  onssi  4360  onsuci  4361  ordtriexmidlem  4364  ordtriexmidlem2  4365  ordtriexmid  4366  ordtri2orexmid  4367  2ordpr  4368  ontr2exmid  4369  onsucsssucexmid  4371  onsucelsucexmid  4374  regexmidlemm  4376  reg2exmid  4380  onirri  4387  ruALT  4395  onprc  4396  sucon  4397  dtru  4404  0elsucexmid  4409  ordpwsucexmid  4414  ordtri2or2exmid  4415  dcextest  4424  omex  4436  find  4442  omelon  4451  nnoni  4453  limom  4456  nnregexmid  4462  omsinds  4463  xpeq1i  4487  xpeq2i  4488  0nelxp  4495  opthprc  4518  mosubop  4533  releqi  4550  relssi  4558  relin1  4585  relin2  4586  reldif  4587  inopab  4599  difopab  4600  xpiindim  4604  opabbi2dv  4616  ideq  4619  coeq1i  4626  coeq2i  4627  cnveqi  4642  eldm  4664  eldm2  4665  dmeqi  4668  dmv  4683  rneqi  4695  elrnmpti  4720  dmex  4731  rnex  4732  reseq1i  4741  reseq2i  4742  residm  4777  resex  4786  resmpt3  4794  imaeq1i  4804  imaeq2i  4805  elima  4812  imaex  4820  elimasn  4832  args  4834  epini  4836  dfse2  4838  relbrcnv  4845  cotr  4846  issref  4847  cnvsym  4848  asymref  4850  intirr  4851  codir  4853  qfto  4854  ssrnres  4907  cnveq0  4921  cnvsn0  4933  dmsnop  4938  rnsnop  4945  resdm2  4955  dfco2a  4965  cocnvcnv1  4975  coi2  4981  coires1  4982  cnvssrndm  4986  cossxp  4987  cocnvres  4989  relrelss  4991  relcoi2  4995  unidmrn  4997  dfdm2  4999  unixpm  5000  cnvexg  5002  cnvex  5003  cnviinm  5006  iotaval  5025  funeqi  5070  funi  5080  funres  5089  funcnvsn  5093  funcnvcnv  5107  funin  5119  funcnvres  5121  isarep2  5135  fneq1i  5142  fneq2i  5143  fnresdisj  5158  fnresi  5165  mpt0  5175  dmmpti  5177  feq1i  5188  feq2i  5189  fdmi  5203  fun2  5219  fssres  5221  resasplitss  5225  fintm  5231  fconst6  5245  f1ores  5303  foimacnv  5306  resdif  5310  funcocnv2  5313  f1ovi  5327  fveq1i  5341  fveq2i  5343  0fv  5374  fvun1  5405  fvopab3ig  5413  fvmptss2  5414  mptrcl  5421  elfvmptrab1  5433  fndmdif  5443  fneqeql2  5447  f1oresrab  5502  fmptco  5503  fnressn  5522  fressnfv  5523  fmptap  5526  fvsnun1  5533  fvsnun2  5534  fsnunfv  5537  fconst2  5553  mptex  5562  riotabiia  5663  acexmidlema  5681  acexmidlemb  5682  acexmidlemcase  5685  acexmidlem2  5687  acexmidlemv  5688  oveq1i  5700  oveq2i  5701  oveqi  5703  oprabidlem  5718  0neqopab  5732  oprabbii  5742  oprabss  5772  mpt2mpt  5778  funoprab  5783  fnoprab  5786  fovcl  5788  ovigg  5803  elmpt2cl  5880  resfunexgALT  5919  cofunexg  5920  opabex3d  5930  opabex3  5931  1st0  5953  2nd0  5954  op1st  5955  op2nd  5956  f1stres  5968  f2ndres  5969  fo1stresm  5970  fo2ndresm  5971  1stcof  5972  2ndcof  5973  1stexg  5976  2ndexg  5977  releldm2  5993  reldm  5994  dfoprab3  5999  mpt2mptsx  6005  mpt2mpts  6006  fnmpt2i  6012  dmmpt2  6013  mpt2exxg  6015  1stconst  6024  2ndconst  6025  dfmpt2  6026  algrflem  6032  algrflemg  6033  cnvoprab  6037  f1od2  6038  mpt2xopn0yelv  6042  mpt2xopoveq  6043  tposssxp  6052  brtpos2  6054  reldmtpos  6056  dftpos2  6064  dftpos4  6066  tpostpos  6067  tpostpos2  6068  tposfo  6074  tposf  6075  tposeqi  6080  tposex  6081  tposoprab  6083  issmo  6091  smores  6095  smores2  6097  iordsmo  6100  smo0  6101  tfrlem8  6121  tfrexlem  6137  tfr1onlem3  6141  tfr1onlemsucaccv  6144  tfr1onlembxssdm  6146  tfr1onlemres  6152  tfri1dALT  6154  tfri2  6169  rdgisuc1  6187  rdg0  6190  frecfun  6198  frec0g  6200  freccllem  6205  frecfcllem  6207  frecsuclem  6209  frecrdg  6211  2on0  6229  xp01disj  6236  2oconcl  6241  fnoa  6248  oaexg  6249  fnom  6251  omexg  6252  fnoei  6253  oeiexg  6254  oei0  6260  oacl  6261  oasuc  6265  o1p1e2  6269  omsuc  6273  nna0r  6279  nnm0r  6280  1onn  6319  2onn  6320  3onn  6321  4onn  6322  eqerlem  6363  elqs  6383  qsex  6389  ecqs  6394  iinerm  6404  th3qlem1  6434  th3q  6437  mapsn  6487  mapsnf1o3  6494  ixpiinm  6521  ixpssmap  6529  brdom  6547  f1dom  6557  enref  6562  dom2  6572  idssen  6574  ssdomg  6575  ensymi  6579  ensn1  6593  fiprc  6612  1domsn  6615  xpcomf1o  6621  xpcomco  6622  dom0  6634  0dom  6635  xpmapenlem  6645  phplem2  6649  php5  6654  snnen2og  6655  1nen2  6657  php5dom  6659  ssfilem  6671  ssfiexmid  6672  domfiexmid  6674  0fin  6680  diffitest  6683  findcard  6684  findcard2  6685  findcard2s  6686  isinfinf  6693  ac6sfi  6694  inffiexmid  6702  unfiexmid  6708  xpfi  6720  fisseneq  6722  ssfirab  6723  en1eqsn  6737  snexxph  6739  sbthlem2  6747  sbthlemi3  6748  sbthlemi6  6751  sbthlem7  6752  supeq1i  6763  infeq1i  6788  djuf1olemr  6826  inresflem  6832  djuinr  6835  djuun  6840  updjudhcoinlf  6851  updjudhcoinrg  6852  casefun  6856  caserel  6858  caseinj  6860  caseinl  6862  djuinj  6868  0ct  6869  ctmlemr  6870  finomni  6883  exmidomniim  6884  exmidomni  6885  fodjuomni  6892  nnnninf  6894  fodjumkv  6903  card0  6913  dju1p1e2  6920  exmidfodomrlemim  6924  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  0npi  6969  dmaddpi  6981  dmmulpi  6982  1lt2pi  6996  0nnq  7020  1nq  7022  dmaddpq  7035  dmmulpq  7036  rec1nq  7051  1lt2nq  7062  halfnqq  7066  prarloclemarch2  7075  enq0enq  7087  nqnq0pi  7094  nnnq0lem1  7102  addnnnq0  7105  mulnnnq0  7106  nq0m0r  7112  addpinq1  7120  prarloclem5  7156  prarloclemcalc  7158  1pr  7210  1idprl  7246  1idpru  7247  ltexprlemm  7256  recexprlem1ssl  7289  recexprlem1ssu  7290  prsrlem1  7385  addsrpr  7388  mulsrpr  7389  gt0srpr  7391  0nsr  7392  0r  7393  1sr  7394  m1r  7395  m1m1sr  7404  caucvgsr  7444  addresr  7471  mulresr  7472  pitonnlem1  7479  peano1nnnn  7486  axi2m1  7507  axcnre  7513  peano5nnnn  7524  axcaucvg  7532  mulid1i  7587  mulid2i  7588  pnfnre  7626  mnfnre  7627  pnfnemnf  7639  mnfxr  7641  rexri  7642  ltnri  7674  ltleii  7684  00id  7720  addid1i  7721  addid2i  7722  0cnALT  7769  negeqi  7773  negicn  7780  neg0  7825  renegcli  7841  negcli  7847  negidi  7848  negnegi  7849  subidi  7850  subid1i  7851  negne0bi  7852  negrebi  7853  mul02i  7965  mul01i  7966  mulm1i  7978  leidi  8060  gt0ne0ii  8062  inelr  8158  msqge0i  8191  gt0ap0ii  8201  1div1e1  8268  div1i  8304  eqnegi  8305  recclapi  8306  recidapi  8307  divmulapi  8330  rerecclapi  8341  redivclapi  8343  recgt0  8408  ltp1i  8463  divgt0ii  8477  ltmul1ii  8486  ltdiv1ii  8487  sup3exmid  8515  peano5nni  8523  nnrei  8529  1nn  8531  nngt0i  8550  neg1ap0  8629  2timesi  8644  times2i  8645  2nn  8675  3nn  8676  4nn  8677  5nn  8678  6nn  8679  7nn  8680  8nn  8681  9nn  8682  2muline0  8739  rehalfcli  8762  nn0ssre  8775  nnnn0i  8779  dfn2  8784  0nn0  8786  nn0ge0i  8798  zrei  8854  neg1z  8880  nn0negzi  8883  dfz2  8917  nneoi  8949  peano5uzi  8954  dfuzi  8955  nn0ind-raph  8962  deceq1i  8982  deceq2i  8983  10nn  8991  numltc  9001  eluzel2  9123  eluz1i  9125  nn0uz  9152  nnuz  9153  infrenegsupex  9181  lbzbi  9200  divfnzn  9205  qdivcl  9227  irrmul  9231  cnref1o  9232  0ltpnf  9351  mnflt0  9353  0lepnf  9359  xrltnsym  9362  xrlttri3  9366  nltpnft  9380  ngtmnft  9383  xrrebnd  9385  xnegmnf  9395  xneg0  9397  xltnegi  9401  xaddmnf1  9414  xaddmnf2  9415  mnfaddpnf  9417  xaddid1  9428  xnn0lenn0nn0  9431  xnn0xadd0  9433  xposdif  9448  ixxex  9465  iooval2  9481  unirnioo  9539  ioorebasg  9541  elrege0  9542  fzval2  9576  fzen  9606  fzprval  9645  fztpval  9646  uzdisj  9656  ige2m1fz  9673  fz01or  9674  fz1ssfz0  9680  fz0tp  9684  nn0disj  9698  1fv  9699  4fvwrd4  9700  fzo0ss1  9734  fzo01  9776  fzo12sn  9777  fzo0to2pr  9778  fzo0to3tp  9779  fzo0to42pr  9780  qbtwnxr  9818  flval  9828  modqfrac  9893  modqmulnn  9898  q2txmodxeq0  9940  frecuzrdgdom  9974  frecuzrdgfun  9976  frecuzrdgsuct  9980  frechashgf1o  9984  nnct  9991  fxnn0nninf  9993  0tonninf  9994  1tonninf  9995  iseqvalcbv  10018  ser0f  10081  0exp0e1  10091  qexpcl  10102  qexpclz  10107  m1expcl2  10108  1exp  10115  sqvali  10165  sqcli  10166  sqeq0i  10167  resqcli  10170  sq1  10179  neg1sqe1  10180  iexpcyc  10190  facnn  10266  fac0  10267  fac1  10268  fac2  10270  fac3  10271  fac4  10272  bcval  10288  bcm1k  10299  bcpasc  10305  bccl  10306  4bc3eq4  10312  4bc2eq6  10313  hashinfom  10317  hashennn  10319  hashfz1  10322  fihasheq0  10333  hash0  10336  hashsng  10337  fihashen1  10338  omgadd  10341  hashp1i  10349  hashxp  10365  fimaxq  10366  zfz1iso  10377  shftidt2  10397  cjexp  10458  re0  10460  im0  10461  re1  10462  im1  10463  cj0  10466  cji  10467  recli  10476  imcli  10477  cjcli  10478  replimi  10479  cjcji  10480  reim0bi  10481  rerebi  10482  cjrebi  10483  recji  10484  imcji  10485  cjmulrcli  10486  cjmulvali  10487  cjmulge0i  10488  renegi  10489  imnegi  10490  cjnegi  10491  addcji  10492  uzin2  10551  rexanuz  10552  rexfiuz  10553  sqrtrval  10564  sqrt0  10568  resqrexlemcalc3  10580  resqrexlemcvg  10583  resqrex  10590  abs0  10622  absi  10623  qabsor  10639  absimle  10648  recan  10673  caubnd2  10681  leabsi  10692  absrei  10693  sqrtpclii  10694  sqrtgt0ii  10695  absvalsqi  10704  absvalsq2i  10705  abscli  10706  absge0i  10707  absval2i  10708  abs00i  10709  absgt0api  10710  absnegi  10711  abscji  10712  releabsi  10713  infxrnegsupex  10822  xrbdtri  10835  cbvsum  10919  sumeq1i  10922  sum0  10947  isumz  10948  fisumss  10951  fsumsersdc  10954  fsumadd  10965  isumclim  10980  isumclim3  10982  fsumcnv  10996  modfsummodlem1  11015  fsumrelem  11030  binomlem  11042  binom  11043  arisum2  11058  expcnv  11063  0.999...  11080  ef0lem  11115  esum  11117  ere  11125  ege2le3  11126  ef0  11127  eff2  11135  efsep  11146  reeff1  11156  sin0  11185  cos0  11186  ef01bndlem  11212  cos2bnd  11216  sincos1sgn  11220  sincos2sgn  11221  sin4lt0  11222  eirr  11231  0dvds  11259  dvds1  11297  z0even  11354  n2dvdsm1  11356  z2even  11357  n2dvds3  11358  ndvdssub  11373  ndvdsi  11376  flodddiv4  11377  gcddvds  11398  gcd1  11421  6gcd4e2  11427  bezoutlembi  11437  dfgcd3  11442  dfgcd2  11446  lcmval  11488  lcmcllem  11492  lcmledvds  11495  3lcm2e6woprm  11511  qredeu  11522  isprm2lem  11541  isprm3  11543  prm2orodd  11551  pw2dvds  11587  phicl2  11633  phi1  11638  dfphi2  11639  phiprmpw  11641  structcnvcnv  11675  structfun  11677  structfn  11678  ndxarg  11682  ndxid  11683  setsresg  11697  setsslnid  11710  strleun  11748  strle1g  11749  istopon  11880  topontopi  11883  toponunii  11884  istps  11898  topontopn  11903  eltpsi  11907  eltg4i  11923  eltg3  11925  tg1  11927  tg2  11928  tgclb  11933  topnex  11954  sn0topon  11956  distps  11959  cldrcl  11970  sn0cld  12005  restco  12042  lmrcl  12059  ssidcn  12077  cnconst2  12100  cnptopresti  12105  cnptoprest  12106  cnmptid  12119  psmetge0  12133  ismeti  12148  xmetunirn  12160  xmetge0  12167  unirnblps  12224  unirnbl  12225  mopnex  12307  qtopbasss  12316  retop  12319  uniretop  12320  iooretopg  12323  cnxmet  12326  cnbl0  12327  rexmet  12331  blssioo  12335  tgioo  12336  tgqioo  12337  ex-fl  12376  ex-ceil  12377  ex-exp  12378  ex-fac  12379  ex-gcd  12382  elabf2  12406  bd0  12439  bdeli  12461  bdcriota  12498  bdbm1.3ii  12506  bdinex1  12514  bdssexi  12518  bj-inex  12522  bj-snex  12528  bj-sucex  12538  bj-notbii  12541  bj-d0clsepcl  12544  bj-omind  12553  bj-om  12556  bj-2inf  12557  bj-peano2  12558  bdpeano5  12562  bj-omssonALT  12582  bj-inf2vnlem1  12589  bj-omex2  12596  bj-nn0sucALT  12597  nninfall  12621  nninfsellemqall  12628  nninfsellemeqinf  12629  nninfomnilem  12631  nninfomni  12632  exmidsbthrlem  12633