ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-mp Structured version   Unicode version

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
StepHypRef Expression
1 wps 1
Colors of variables: wff set class
This axiom is referenced by:  mp2b  8  a1i  9  mp1i  10  a2i  11  mpd  13  mp2  16  id1  20  simpli  104  simpri  106  biimpi  113  bicomi  123  mpbi  133  mpbir  134  imbi1i  227  a1bi  232  tbt  236  biantru  286  biantrur  287  mp2an  402  pm2.65i  567  notnoti  573  pm2.21i  574  pm2.24ii  575  notbii  593  nbn  614  ori  641  orci  649  olci  650  biorfi  664  imorri  667  simp1i  912  simp2i  913  simp3i  914  3mix1i  1075  3mix2i  1076  3mix3i  1077  3jaoi  1197  trud  1251  dfnot  1261  mpto1  1311  mtp-xor  1313  mtp-or  1314  mpg  1337  19.23h  1384  hbequid  1403  axi12  1404  nfri  1409  spi  1426  19.21  1472  eximii  1490  19.35i  1513  nfn  1545  19.37aiv  1562  19.23  1565  exan  1580  equid  1586  hbae  1603  equvini  1638  equveli  1639  sbid  1654  sbieh  1670  exdistrfor  1678  dveeq2or  1694  ax11v  1705  ax11ev  1706  equs5or  1708  sb4or  1711  sb4bor  1713  nfsb2or  1715  sbequilem  1716  sbequi  1717  speiv  1739  nfsbxy  1815  nfsbxyt  1816  sbco  1839  sbcocom  1841  sbcomxyyz  1843  elsb3  1849  elsb4  1850  sbal1yz  1874  dvelimALT  1883  dvelimfv  1884  dvelimor  1891  eumoi  1930  moani  1967  eqeq1i  2044  eqeq2i  2047  eleq1i  2100  eleq2i  2101  nfcrii  2168  neeq1i  2215  neeq2i  2216  necon3i  2247  rspec  2367  rgen2a  2369  mprg  2372  r19.21  2389  r19.23  2418  raleqi  2503  rexeqi  2504  elexi  2561  ceqsal  2577  vtocl3  2604  vtoclef  2620  vtocle  2621  spcv  2640  spcev  2641  clel3  2673  elabf  2680  elab2  2684  elab3  2688  euxfrdc  2721  reueq  2732  rmoimi2  2736  sbsbc  2762  sbc8g  2765  sbc6  2783  sbcie  2791  csbvarg  2871  csbief  2885  csbie2  2889  sbnfc2  2900  sseli  2935  sselii  2936  sseq1i  2963  sseq2i  2964  psseq1i  3027  psseq2i  3028  difeq1i  3052  difeq2i  3053  uneq1i  3087  uneq2i  3088  ineq1i  3128  ineq2i  3129  ssinss1  3159  difdif2ss  3188  vn0  3225  vn0m  3226  abf  3254  npss0  3260  disj2  3269  difid  3286  0dif  3289  disjdif  3290  difin0  3291  undif1ss  3292  difdifdirss  3301  rgenm  3317  iftruei  3331  iffalsei  3334  ifbieq2i  3345  ifbieq12i  3347  pweqi  3355  pwid  3365  sneqi  3379  elpr  3385  elsnc  3390  elsnc2  3397  ralsn  3405  rexsn  3406  eltp  3409  r19.12sn  3427  rabrsndc  3429  preq1i  3441  preq2i  3442  prid1  3467  snnz  3478  snm  3479  prnz  3481  prm  3482  tpnz  3484  snsssn  3523  opeq1i  3543  opeq2i  3544  unieqi  3581  unissi  3594  inteqi  3610  intmin2  3632  intab  3635  intsn  3641  iinconstm  3657  iuniin  3658  iinss1  3660  iunxdif2  3696  ssiinf  3697  iinss  3699  iinss2  3700  iinab  3709  iundif2ss  3713  iindif2m  3715  iinin2m  3716  iunxsn  3724  iinpw  3733  sndisj  3751  disjxsn  3753  breqi  3761  breq1i  3762  breq2i  3763  brab1  3800  opabbii  3815  truni  3859  bm1.3ii  3869  a9evsep  3870  ax9vsep  3871  zfnuleu  3872  axnul  3873  ssexi  3886  rabex  3892  elpw2  3902  pwnss  3903  iin0r  3913  intv  3914  snex  3928  ord3ex  3932  dtruarb  3933  snelpw  3940  rext  3942  sspwb  3943  intid  3951  euabex  3952  mss  3953  exss  3954  opi1  3960  opnzi  3963  copsexg  3972  opeqsn  3980  opeqpr  3981  uniop  3983  opelopabf  4002  epelc  4019  elon  4077  inton  4096  onn0  4103  onm  4104  elsuc  4109  elsuc2  4110  sucid  4120  iunsuc  4123  onordi  4129  ontrci  4130  onelssi  4132  snnex  4147  eusvnf  4151  op1stb  4175  ssonunii  4181  sucex  4191  onssi  4206  onsuci  4207  ordtriexmidlem  4208  ordtriexmidlem2  4209  ordtriexmid  4210  ordtri2orexmid  4211  onsucsssucexmid  4212  onsucelsucexmidlem  4214  onsucelsucexmid  4215  regexmidlemm  4217  ruALT  4229  onprc  4230  sucon  4231  dtruex  4237  dtru  4238  ordpwsucexmid  4246  omex  4259  find  4265  omelon  4274  nnoni  4276  limom  4279  nnregexmid  4285  xpeq1i  4308  xpeq2i  4309  0nelxp  4315  opthprc  4334  mosubop  4349  releqi  4366  relssi  4374  relin1  4398  relin2  4399  reldif  4400  inopab  4411  difopab  4412  xpiindim  4416  opabbi2dv  4428  relop  4429  ideq  4431  coeq1i  4438  coeq2i  4439  cnveqi  4453  eldm  4475  eldm2  4476  dmeqi  4479  dmv  4494  rneqi  4505  elrnmpti  4530  dmex  4541  rnex  4542  reseq1i  4551  reseq2i  4552  residm  4585  resex  4594  resmpt3  4600  imaeq1i  4608  imaeq2i  4609  elima  4616  elimasn  4635  args  4637  epini  4639  dfse2  4641  relbrcnv  4648  cotr  4649  issref  4650  cnvsym  4651  asymref  4653  intirr  4654  codir  4656  qfto  4657  ssrnres  4706  cnveq0  4720  cnvsn0  4732  dmsnop  4737  rnsnop  4744  resdm2  4754  dfco2a  4764  cocnvcnv1  4774  coi2  4780  coires1  4781  cnvssrndm  4785  cossxp  4786  relrelss  4787  relcoi2  4791  unidmrn  4793  dfdm2  4795  unixpm  4796  cnvexg  4798  cnvex  4799  cnviinm  4802  iotaval  4821  funeqi  4865  funi  4875  funopg  4877  funres  4884  funcnvsn  4888  funcnvcnv  4901  funin  4913  funcnvres  4915  isarep2  4929  fneq1i  4936  fneq2i  4937  fnresdisj  4952  fnresi  4959  mpt0  4969  dmmpti  4971  feq1i  4982  feq2i  4983  fdmi  4994  fun2  5007  fssres  5009  resasplitss  5012  fintm  5018  fconst6  5029  f1ores  5084  foimacnv  5087  resdif  5091  funcocnv2  5094  f1ovi  5108  fveq1i  5122  fveq2i  5124  0fv  5151  fvun1  5182  fvopab3ig  5189  fvmptss2  5190  fndmdif  5215  fneqeql2  5219  f1oresrab  5272  fmptco  5273  fnressn  5292  fressnfv  5293  fmptap  5296  fvsnun1  5303  fvsnun2  5304  fsnunfv  5306  fconst2  5321  mptex  5330  riotabiia  5428  acexmidlema  5446  acexmidlemb  5447  acexmidlemcase  5450  acexmidlem2  5452  acexmidlemv  5453  oveq1i  5465  oveq2i  5466  oveqi  5468  oprabidlem  5479  0neqopab  5492  oprabbii  5502  oprabss  5532  mpt2mpt  5538  funoprab  5543  fnoprab  5546  fovcl  5548  ovigg  5563  elmpt2cl  5640  resfunexgALT  5679  cofunexg  5680  opabex3d  5690  opabex3  5691  1st0  5713  2nd0  5714  op1st  5715  op2nd  5716  fo1st  5726  fo2nd  5727  f1stres  5728  f2ndres  5729  fo1stresm  5730  fo2ndresm  5731  1stcof  5732  2ndcof  5733  1stexg  5736  2ndexg  5737  releldm2  5753  reldm  5754  dfoprab3  5759  mpt2mptsx  5765  mpt2mpts  5766  fnmpt2i  5772  dmmpt2  5773  mpt2exxg  5775  1stconst  5784  2ndconst  5785  dfmpt2  5786  algrflem  5792  mpt2xopn0yelv  5795  mpt2xopoveq  5796  tposssxp  5805  brtpos2  5807  reldmtpos  5809  dftpos2  5817  dftpos4  5819  tpostpos  5820  tpostpos2  5821  tposfo  5827  tposf  5828  tposeqi  5833  tposex  5834  tposoprab  5836  issmo  5844  smores  5848  smores2  5850  iordsmo  5853  smo0  5854  tfrlem8  5875  tfrexlem  5889  tfri2  5893  rdgisuc1  5911  rdg0  5914  frec0g  5922  frecsuclem1  5926  frecsuclem2  5928  frecrdg  5931  2on0  5949  xp01disj  5956  2oconcl  5961  fnoa  5966  oaexg  5967  fnom  5969  omexg  5970  fnoei  5971  oeiexg  5972  oei0  5978  oacl  5979  oasuc  5983  o1p1e2  5987  omsuc  5990  nna0r  5996  nnm0r  5997  1onn  6029  2onn  6030  3onn  6031  4onn  6032  eqerlem  6073  elqs  6093  qsex  6099  ecqs  6104  iinerm  6114  th3qlem1  6144  th3q  6147  brdom  6167  f1dom  6176  enref  6181  dom2  6191  idssen  6193  ssdomg  6194  ensymi  6198  ensn1  6212  fiprc  6228  xpcomf1o  6235  xpcomco  6236  ssfiexmid  6254  0fin  6255  0npi  6297  dmaddpi  6309  dmmulpi  6310  1lt2pi  6324  0nnq  6348  1nq  6350  dmaddpq  6363  dmmulpq  6364  rec1nq  6379  1lt2nq  6389  halfnqq  6393  prarloclemarch2  6402  enq0enq  6413  nqnq0pi  6420  nnnq0lem1  6428  addnnnq0  6431  mulnnnq0  6432  nq0m0r  6438  addpinq1  6446  prarloclem5  6482  prarloclemcalc  6484  1pr  6534  1idprl  6564  1idpru  6565  ltexprlemm  6572  recexprlem1ssl  6603  recexprlem1ssu  6604  prsrlem1  6630  addsrpr  6633  mulsrpr  6634  gt0srpr  6636  0nsr  6637  0r  6638  1sr  6639  m1r  6640  m1m1sr  6649  addresr  6694  mulresr  6695  pitonnlem1  6701  axi2m1  6719  axcnre  6725  mulid1i  6787  mulid2i  6788  pnfnre  6824  mnfnre  6825  rexri  6835  ltnri  6867  ltleii  6877  00id  6911  addid1i  6912  addid2i  6913  0cnALT  6958  negeqi  6962  negicn  6969  neg0  7013  renegcli  7029  negcli  7035  negidi  7036  negnegi  7037  subidi  7038  subid1i  7039  negne0bi  7040  negrebi  7041  mul02i  7143  mul01i  7144  mulm1i  7156  leidi  7232  gt0ne0ii  7234  inelr  7328  msqge0i  7361  gt0ap0ii  7370  1div1e1  7423  div1i  7458  eqnegi  7459  recclapi  7460  recidapi  7461  divmulapi  7484  rerecclapi  7495  redivclapi  7497  recgt0  7557  ltp1i  7612  divgt0ii  7626  ltmul1ii  7635  ltdiv1ii  7636  peano5nni  7658  nnrei  7664  1nn  7666  nngt0i  7685  neg1ap0  7764  2timesi  7778  times2i  7779  2nn  7815  3nn  7816  4nn  7817  5nn  7818  6nn  7819  7nn  7820  8nn  7821  9nn  7822  10nn  7823  2muline0  7887  rehalfcli  7910  nn0ssre  7921  nnnn0i  7925  dfn2  7930  0nn0  7932  nn0ge0i  7945  zrei  7987  neg1z  8013  nn0negzi  8016  dfz2  8049  nneoi  8078  peano5uzi  8083  dfuzi  8084  nn0ind-raph  8091  deceq1i  8108  deceq2i  8109  numltc  8123  eluzel2  8214  eluz1i  8216  nn0uz  8243  nnuz  8244  lbzbi  8287  divfnzn  8292  qdivcl  8312  irrmul  8316  cnref1o  8317  mnfxr  8424  pnfnemnf  8427  0ltpnf  8433  mnflt0  8435  0lepnf  8441  xrltnsym  8444  xrlttri3  8448  nltpnft  8460  ngtmnft  8461  xrrebnd  8462  xnegmnf  8472  xneg0  8474  xltnegi  8478  ixxex  8498  iooval2  8514  unirnioo  8572  ioorebasg  8574  elrege0  8575  fzval2  8607  fzen  8637  fzprval  8674  fztpval  8675  uzdisj  8685  ige2m1fz  8702  fz0tp  8711  nn0disj  8725  1fv  8726  4fvwrd4  8727  fzo0ss1  8760  fzo01  8802  fzo12sn  8803  fzo0to2pr  8804  fzo0to3tp  8805  fzo0to42pr  8806  frechashgf1o  8846  0exp0e1  8874  qexpcl  8885  qexpclz  8890  m1expcl2  8891  1exp  8898  sqvali  8946  sqcli  8947  sqeq0i  8948  resqcli  8951  sq1  8960  neg1sqe1  8961  cjexp  9081  re0  9083  im0  9084  re1  9085  im1  9086  cj0  9089  cji  9090  recli  9099  imcli  9100  cjcli  9101  replimi  9102  cjcji  9103  reim0bi  9104  rerebi  9105  cjrebi  9106  recji  9107  imcji  9108  cjmulrcli  9109  cjmulvali  9110  cjmulge0i  9111  renegi  9112  imnegi  9113  cjnegi  9114  addcji  9115  elabf2  9190  bd0  9213  bdeli  9235  bdcriota  9272  bdbm1.3ii  9279  bdinex1  9284  bdssexi  9288  bj-inex  9292  bj-snex  9298  bj-sucex  9308  bj-notbii  9311  bj-d0clsepcl  9314  bj-omind  9322  bj-om  9325  bj-2inf  9326  bj-peano2  9327  bdpeano5  9331  bj-inf2vnlem1  9354  bj-omex2  9361  bj-nn0sucALT  9362
  Copyright terms: Public domain W3C validator