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 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.

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	|- 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  109  simpri  111  biimpi  118  bicomi  130  mpbi  143  mpbir  144  imbi1i  236  a1bi  241  tbt  245  biantru  296  biantrur  297  mp2an  416  pm2.65i  600  notnoti  606  pm2.21i  607  pm2.24ii  608  notbii  626  nbn  647  ori  674  orci  682  olci  683  biorfi  697  imorri  700  simp1i  947  simp2i  948  simp3i  949  3mix1i  1110  3mix2i  1111  3mix3i  1112  3jaoi  1234  trud  1293  dfnot  1302  mptnan  1354  mtpor  1356  mtpxor  1357  mpg  1380  19.23h  1427  hbequid  1446  axi12  1447  nfri  1452  spi  1469  19.21  1515  eximii  1533  19.35i  1556  nfn  1588  19.37aiv  1605  19.23  1608  exan  1623  equid  1629  hbae  1646  equvini  1681  equveli  1682  sbid  1697  sbieh  1713  exdistrfor  1721  dveeq2or  1737  ax11v  1748  ax11ev  1749  equs5or  1751  sb4or  1754  sb4bor  1756  nfsb2or  1758  sbequilem  1759  sbequi  1760  speiv  1783  nfsbxy  1859  nfsbxyt  1860  sbco  1883  sbcocom  1885  sbcomxyyz  1887  elsb3  1893  elsb4  1894  sbal1yz  1918  dvelimALT  1927  dvelimfv  1928  dvelimor  1935  eumoi  1974  moani  2011  eqeq1i  2088  eqeq2i  2091  eleq1i  2144  eleq2i  2145  nfcrii  2212  neeq1i  2260  neeq2i  2261  necon3i  2293  rspec  2415  rgen2a  2417  mprg  2420  r19.21  2437  r19.23  2468  raleqi  2553  rexeqi  2554  elexi  2611  ceqsal  2628  vtocl3  2655  vtoclef  2671  vtocle  2672  spcv  2691  spcev  2692  clel3  2730  elabf  2737  elab2  2741  elab3  2745  euxfrdc  2778  reueq  2789  rmoimi2  2793  sbsbc  2819  sbc8g  2822  sbc6  2840  sbcie  2848  sbcrex  2893  csbvarg  2933  csbief  2947  csbie2  2951  sbnfc2  2962  sseli  2995  sselii  2996  sseq1i  3023  sseq2i  3024  difeq1i  3086  difeq2i  3087  uneq1i  3122  uneq2i  3123  ineq1i  3163  ineq2i  3164  ssinss1  3194  difdif2ss  3221  vn0  3258  vn0m  3259  abf  3287  disj2  3299  difid  3312  0dif  3315  disjdif  3316  difin0  3317  undif1ss  3318  difdifdirss  3327  rgenm  3343  iftruei  3357  iffalsei  3360  ifbieq2i  3372  ifbieq12i  3374  pweqi  3386  pwid  3396  sneqi  3410  elsn  3414  elpr  3419  elsn2  3428  ralsn  3436  rexsn  3437  eltp  3440  rabrsndc  3460  preq1i  3472  preq2i  3473  prid1  3498  snnz  3509  snm  3510  prnz  3512  prm  3513  tpnz  3515  snsssn  3553  opeq1i  3573  opeq2i  3574  unieqi  3611  unissi  3624  inteqi  3640  intmin2  3662  intab  3665  intsn  3671  iinconstm  3687  iuniin  3688  iinss1  3690  iunxdif2  3726  ssiinf  3727  iinss  3729  iinss2  3730  iinab  3739  iundif2ss  3743  iindif2m  3745  iinin2m  3746  iunxsn  3754  iinpw  3763  sndisj  3781  disjxsn  3783  breqi  3791  breq1i  3792  breq2i  3793  brab1  3830  opabbii  3845  truni  3889  bm1.3ii  3899  a9evsep  3900  ax9vsep  3901  zfnuleu  3902  axnul  3903  ssexi  3916  rabex  3922  elpw2  3932  pwnss  3933  iin0r  3943  intv  3944  snex  3957  ord3ex  3961  dtruarb  3962  intid  3979  opnzi  3990  copsexg  3999  opelopabf  4029  epelc  4046  elon  4129  inton  4148  onn0  4155  onm  4156  elsuc  4161  elsuc2  4162  sucid  4172  iunsuc  4175  onordi  4181  ontrci  4182  onelssi  4184  eusvnf  4203  ssonunii  4233  sucex  4243  onssi  4259  onsuci  4260  ordtriexmidlem  4263  ordtriexmidlem2  4264  ordtriexmid  4265  ordtri2orexmid  4266  2ordpr  4267  ontr2exmid  4268  onsucsssucexmid  4270  onsucelsucexmid  4273  regexmidlemm  4275  reg2exmid  4279  onirri  4286  ruALT  4294  onprc  4295  sucon  4296  dtru  4303  0elsucexmid  4308  ordpwsucexmid  4313  ordtri2or2exmid  4314  omex  4334  find  4340  omelon  4349  nnoni  4351  limom  4354  nnregexmid  4360  xpeq1i  4383  xpeq2i  4384  0nelxp  4390  opthprc  4409  mosubop  4424  releqi  4441  relssi  4449  relin1  4473  relin2  4474  reldif  4475  inopab  4486  difopab  4487  xpiindim  4491  opabbi2dv  4503  ideq  4506  coeq1i  4513  coeq2i  4514  cnveqi  4528  eldm  4550  eldm2  4551  dmeqi  4554  dmv  4569  rneqi  4580  elrnmpti  4605  dmex  4616  rnex  4617  reseq1i  4626  reseq2i  4627  residm  4660  resex  4669  resmpt3  4677  imaeq1i  4685  imaeq2i  4686  elima  4693  elimasn  4712  args  4714  epini  4716  dfse2  4718  relbrcnv  4725  cotr  4726  issref  4727  cnvsym  4728  asymref  4730  intirr  4731  codir  4733  qfto  4734  ssrnres  4783  cnveq0  4797  cnvsn0  4809  dmsnop  4814  rnsnop  4821  resdm2  4831  dfco2a  4841  cocnvcnv1  4851  coi2  4857  coires1  4858  cnvssrndm  4862  cossxp  4863  relrelss  4864  relcoi2  4868  unidmrn  4870  dfdm2  4872  unixpm  4873  cnvexg  4875  cnvex  4876  cnviinm  4879  iotaval  4898  funeqi  4942  funi  4952  funres  4961  funcnvsn  4965  funcnvcnv  4978  funin  4990  funcnvres  4992  isarep2  5006  fneq1i  5013  fneq2i  5014  fnresdisj  5029  fnresi  5036  mpt0  5046  dmmpti  5048  feq1i  5059  feq2i  5060  fdmi  5071  fun2  5084  fssres  5086  resasplitss  5089  fintm  5095  fconst6  5106  f1ores  5161  foimacnv  5164  resdif  5168  funcocnv2  5171  f1ovi  5185  fveq1i  5199  fveq2i  5201  0fv  5229  fvun1  5260  fvopab3ig  5267  fvmptss2  5268  fndmdif  5293  fneqeql2  5297  f1oresrab  5350  fmptco  5351  fnressn  5370  fressnfv  5371  fmptap  5374  fvsnun1  5381  fvsnun2  5382  fsnunfv  5384  fconst2  5399  mptex  5408  riotabiia  5505  acexmidlema  5523  acexmidlemb  5524  acexmidlemcase  5527  acexmidlem2  5529  acexmidlemv  5530  oveq1i  5542  oveq2i  5543  oveqi  5545  oprabidlem  5556  0neqopab  5570  oprabbii  5580  oprabss  5610  mpt2mpt  5616  funoprab  5621  fnoprab  5624  fovcl  5626  ovigg  5641  elmpt2cl  5718  resfunexgALT  5757  cofunexg  5758  opabex3d  5768  opabex3  5769  1st0  5791  2nd0  5792  op1st  5793  op2nd  5794  f1stres  5806  f2ndres  5807  fo1stresm  5808  fo2ndresm  5809  1stcof  5810  2ndcof  5811  1stexg  5814  2ndexg  5815  releldm2  5831  reldm  5832  dfoprab3  5837  mpt2mptsx  5843  mpt2mpts  5844  fnmpt2i  5850  dmmpt2  5851  mpt2exxg  5853  1stconst  5862  2ndconst  5863  dfmpt2  5864  algrflem  5870  algrflemg  5871  cnvoprab  5875  f1od2  5876  mpt2xopn0yelv  5877  mpt2xopoveq  5878  tposssxp  5887  brtpos2  5889  reldmtpos  5891  dftpos2  5899  dftpos4  5901  tpostpos  5902  tpostpos2  5903  tposfo  5909  tposf  5910  tposeqi  5915  tposex  5916  tposoprab  5918  issmo  5926  smores  5930  smores2  5932  iordsmo  5935  smo0  5936  tfrlem8  5957  tfrexlem  5971  tfri2  5975  rdgisuc1  5994  rdg0  5997  frec0g  6006  frecsuclem1  6010  frecsuclem2  6012  frecrdg  6015  2on0  6033  xp01disj  6040  2oconcl  6045  fnoa  6050  oaexg  6051  fnom  6053  omexg  6054  fnoei  6055  oeiexg  6056  oei0  6062  oacl  6063  oasuc  6067  o1p1e2  6071  omsuc  6074  nna0r  6080  nnm0r  6081  1onn  6116  2onn  6117  3onn  6118  4onn  6119  eqerlem  6160  elqs  6180  qsex  6186  ecqs  6191  iinerm  6201  th3qlem1  6231  th3q  6234  brdom  6254  f1dom  6263  enref  6268  dom2  6278  idssen  6280  ssdomg  6281  ensymi  6285  ensn1  6299  fiprc  6315  xpcomf1o  6322  xpcomco  6323  phplem2  6339  php5  6344  snnen2og  6345  1nen2  6347  php5dom  6349  ssfilem  6360  ssfiexmid  6361  domfiexmid  6363  0fin  6368  diffitest  6371  findcard  6372  findcard2  6373  findcard2s  6374  ac6sfi  6379  supeq1i  6401  infeq1i  6426  card0  6457  0npi  6503  dmaddpi  6515  dmmulpi  6516  1lt2pi  6530  0nnq  6554  1nq  6556  dmaddpq  6569  dmmulpq  6570  rec1nq  6585  1lt2nq  6596  halfnqq  6600  prarloclemarch2  6609  enq0enq  6621  nqnq0pi  6628  nnnq0lem1  6636  addnnnq0  6639  mulnnnq0  6640  nq0m0r  6646  addpinq1  6654  prarloclem5  6690  prarloclemcalc  6692  1pr  6744  1idprl  6780  1idpru  6781  ltexprlemm  6790  recexprlem1ssl  6823  recexprlem1ssu  6824  prsrlem1  6919  addsrpr  6922  mulsrpr  6923  gt0srpr  6925  0nsr  6926  0r  6927  1sr  6928  m1r  6929  m1m1sr  6938  caucvgsr  6978  addresr  7005  mulresr  7006  pitonnlem1  7013  peano1nnnn  7020  axi2m1  7041  axcnre  7047  peano5nnnn  7058  axcaucvg  7066  mulid1i  7121  mulid2i  7122  pnfnre  7160  mnfnre  7161  rexri  7171  ltnri  7203  ltleii  7213  00id  7249  addid1i  7250  addid2i  7251  0cnALT  7298  negeqi  7302  negicn  7309  neg0  7354  renegcli  7370  negcli  7376  negidi  7377  negnegi  7378  subidi  7379  subid1i  7380  negne0bi  7381  negrebi  7382  mul02i  7494  mul01i  7495  mulm1i  7507  leidi  7586  gt0ne0ii  7588  inelr  7684  msqge0i  7717  gt0ap0ii  7727  1div1e1  7792  div1i  7828  eqnegi  7829  recclapi  7830  recidapi  7831  divmulapi  7854  rerecclapi  7865  redivclapi  7867  recgt0  7928  ltp1i  7983  divgt0ii  7997  ltmul1ii  8006  ltdiv1ii  8007  peano5nni  8042  nnrei  8048  1nn  8050  nngt0i  8069  neg1ap0  8148  2timesi  8162  times2i  8163  2nn  8193  3nn  8194  4nn  8195  5nn  8196  6nn  8197  7nn  8198  8nn  8199  9nn  8200  2muline0  8256  rehalfcli  8279  nn0ssre  8292  nnnn0i  8296  dfn2  8301  0nn0  8303  nn0ge0i  8315  zrei  8357  neg1z  8383  nn0negzi  8386  dfz2  8420  nneoi  8451  peano5uzi  8456  dfuzi  8457  nn0ind-raph  8464  deceq1i  8483  deceq2i  8484  10nn  8492  numltc  8502  eluzel2  8624  eluz1i  8626  nn0uz  8653  nnuz  8654  infrenegsupex  8682  lbzbi  8701  divfnzn  8706  qdivcl  8728  irrmul  8732  cnref1o  8733  mnfxr  8848  pnfnemnf  8851  0ltpnf  8857  mnflt0  8859  0lepnf  8865  xrltnsym  8868  xrlttri3  8872  nltpnft  8884  ngtmnft  8885  xrrebnd  8886  xnegmnf  8896  xneg0  8898  xltnegi  8902  ixxex  8922  iooval2  8938  unirnioo  8996  ioorebasg  8998  elrege0  8999  fzval2  9032  fzen  9062  fzprval  9099  fztpval  9100  uzdisj  9110  ige2m1fz  9127  fz0tp  9135  nn0disj  9148  1fv  9149  4fvwrd4  9150  fzo0ss1  9183  fzo01  9225  fzo12sn  9226  fzo0to2pr  9227  fzo0to3tp  9228  fzo0to42pr  9229  qbtwnxr  9266  flval  9276  modqfrac  9339  modqmulnn  9344  q2txmodxeq0  9386  frechashgf1o  9421  nnct  9427  iser0f  9472  0exp0e1  9481  qexpcl  9492  qexpclz  9497  m1expcl2  9498  1exp  9505  sqvali  9555  sqcli  9556  sqeq0i  9557  resqcli  9560  sq1  9569  neg1sqe1  9570  iexpcyc  9579  facnn  9654  fac0  9655  fac1  9656  fac2  9658  fac3  9659  fac4  9660  bcval  9676  bcm1k  9687  ibcval5  9690  bcpasc  9693  bccl  9694  4bc3eq4  9700  4bc2eq6  9701  shftidt2  9720  cjexp  9780  re0  9782  im0  9783  re1  9784  im1  9785  cj0  9788  cji  9789  recli  9798  imcli  9799  cjcli  9800  replimi  9801  cjcji  9802  reim0bi  9803  rerebi  9804  cjrebi  9805  recji  9806  imcji  9807  cjmulrcli  9808  cjmulvali  9809  cjmulge0i  9810  renegi  9811  imnegi  9812  cjnegi  9813  addcji  9814  uzin2  9873  rexanuz  9874  rexfiuz  9875  sqrtrval  9886  sqrt0  9890  resqrexlemcalc3  9902  resqrexlemcvg  9905  resqrex  9912  abs0  9944  absi  9945  qabsor  9961  absimle  9970  recan  9995  caubnd2  10003  leabsi  10014  absrei  10015  sqrtpclii  10016  sqrtgt0ii  10017  absvalsqi  10026  absvalsq2i  10027  abscli  10028  absge0i  10029  absval2i  10030  abs00i  10031  absgt0api  10032  absnegi  10033  abscji  10034  releabsi  10035  0dvds  10215  dvds1  10253  fz01or  10278  z0even  10311  n2dvdsm1  10313  z2even  10314  n2dvds3  10315  ndvdssub  10330  ndvdsi  10333  flodddiv4  10334  gcddvds  10355  gcd1  10378  6gcd4e2  10384  bezoutlembi  10394  dfgcd3  10399  dfgcd2  10403  eucialg  10441  lcmval  10445  lcmcllem  10449  lcmledvds  10452  3lcm2e6woprm  10468  qredeu  10479  isprm2lem  10498  isprm3  10500  prm2orodd  10508  pw2dvds  10544  ex-fl  10563  ex-ceil  10564  ex-fac  10565  ex-gcd  10568  elabf2  10592  bd0  10615  bdeli  10637  bdcriota  10674  bdbm1.3ii  10682  bdinex1  10690  bdssexi  10694  bj-inex  10698  bj-snex  10704  bj-sucex  10714  bj-notbii  10717  bj-d0clsepcl  10720  bj-omind  10729  bj-om  10732  bj-2inf  10733  bj-peano2  10734  bdpeano5  10738  bj-omssonALT  10758  bj-inf2vnlem1  10765  bj-omex2  10772  bj-nn0sucALT  10773