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  552  notnoti  558  pm2.21i  559  pm2.24ii  560  notbii  578  nbn  599  ori  626  orci  634  olci  635  biorfi  649  imorri  652  simp1i  895  simp2i  896  simp3i  897  3mix1i  1058  3mix2i  1059  3mix3i  1060  3jaoi  1179  trud  1232  dfnot  1242  mpto1  1292  mtp-xor  1294  mtp-or  1295  mpg  1313  19.23h  1360  hbequid  1379  axi12  1380  nfri  1385  spi  1402  19.21  1448  eximii  1466  19.35i  1489  nfn  1521  19.37aiv  1538  19.23  1541  exan  1556  equid  1562  hbae  1579  equvini  1614  equveli  1615  sbid  1630  sbieh  1646  exdistrfor  1654  dveeq2or  1670  ax11v  1681  ax11ev  1682  equs5or  1684  sb4or  1687  sb4bor  1689  nfsb2or  1691  sbequilem  1692  sbequi  1693  speiv  1715  nfsbxy  1791  nfsbxyt  1792  sbco  1815  sbcocom  1817  sbcomxyyz  1819  elsb3  1825  elsb4  1826  sbal1yz  1850  dvelimALT  1859  dvelimfv  1860  dvelimor  1867  eumoi  1906  moani  1943  eqeq1i  2020  eqeq2i  2023  eleq1i  2076  eleq2i  2077  nfcrii  2144  neeq1i  2190  neeq2i  2191  necon3i  2222  rspec  2342  rgen2a  2344  mprg  2347  r19.21  2364  r19.23  2393  raleqi  2478  rexeqi  2479  elexi  2535  ceqsal  2551  vtocl3  2578  vtoclef  2594  vtocle  2595  spcv  2614  spcev  2615  clel3  2647  elabf  2654  elab2  2658  elab3  2662  euxfrdc  2695  reueq  2706  rmoimi2  2710  sbsbc  2736  sbc8g  2739  sbc6  2757  sbcie  2765  csbvarg  2845  csbief  2859  csbie2  2863  sbnfc2  2874  sseli  2909  sselii  2910  sseq1i  2937  sseq2i  2938  psseq1i  3001  psseq2i  3002  difeq1i  3026  difeq2i  3027  uneq1i  3061  uneq2i  3062  ineq1i  3102  ineq2i  3103  ssinss1  3133  difdif2ss  3162  vn0  3199  vn0m  3200  abf  3228  npss0  3234  disj2  3243  difid  3260  0dif  3263  disjdif  3264  difin0  3265  undif1ss  3266  difdifdirss  3275  rgenm  3291  iftruei  3305  iffalsei  3307  ifbieq2i  3317  ifbieq12i  3319  pweqi  3327  pwid  3337  sneqi  3351  elpr  3357  elsnc  3362  elsnc2  3369  ralsn  3377  rexsn  3378  eltp  3381  r19.12sn  3399  rabrsndc  3401  preq1i  3413  preq2i  3414  prid1  3439  snnz  3450  snm  3451  prnz  3453  prm  3454  tpnz  3456  snsssn  3495  opeq1i  3515  opeq2i  3516  unieqi  3553  unissi  3566  inteqi  3582  intmin2  3604  intab  3607  intsn  3613  iinconstm  3629  iuniin  3630  iinss1  3632  iunxdif2  3668  ssiinf  3669  iinss  3671  iinss2  3672  iinab  3681  iundif2ss  3685  iindif2m  3687  iinin2m  3688  iunxsn  3696  iinpw  3705  sndisj  3723  disjxsn  3725  breqi  3733  breq1i  3734  breq2i  3735  brab1  3772  opabbii  3787  truni  3831  bm1.3ii  3841  a9evsep  3842  ax9vsep  3843  zfnuleu  3844  axnul  3845  ssexi  3858  rabex  3864  elpw2  3874  pwnss  3875  iin0r  3885  intv  3886  snex  3900  ord3ex  3904  dtruarb  3905  snelpw  3912  rext  3914  sspwb  3915  intid  3923  euabex  3924  mss  3925  exss  3926  opi1  3932  opnzi  3935  copsexg  3944  opeqsn  3952  opeqpr  3953  uniop  3955  opelopabf  3974  epelc  3991  elon  4049  inton  4068  onn0  4075  onm  4076  elsuc  4081  elsuc2  4082  sucid  4092  iunsuc  4095  onordi  4101  ontrci  4102  onelssi  4104  snnex  4119  eusvnf  4123  op1stb  4147  ssonunii  4153  sucex  4163  onssi  4178  onsuci  4179  ordtriexmidlem  4180  ordtriexmidlem2  4181  ordtriexmid  4182  ordtri2orexmid  4183  onsucsssucexmid  4184  onsucelsucexmidlem  4186  onsucelsucexmid  4187  regexmidlemm  4189  ruALT  4201  onprc  4202  sucon  4203  dtruex  4209  dtru  4210  ordpwsucexmid  4218  omex  4231  find  4237  omelon  4246  nnoni  4248  limom  4251  nnregexmid  4257  xpeq1i  4280  xpeq2i  4281  0nelxp  4287  opthprc  4306  mosubop  4321  releqi  4338  relssi  4346  relin1  4370  relin2  4371  reldif  4372  inopab  4383  difopab  4384  xpiindim  4388  opabbi2dv  4400  relop  4401  ideq  4403  coeq1i  4410  coeq2i  4411  cnveqi  4425  eldm  4447  eldm2  4448  dmeqi  4451  dmv  4466  rneqi  4477  elrnmpti  4502  dmex  4513  rnex  4514  reseq1i  4523  reseq2i  4524  residm  4557  resex  4566  resmpt3  4572  imaeq1i  4580  imaeq2i  4581  elima  4588  elimasn  4607  args  4609  epini  4611  dfse2  4613  relbrcnv  4620  cotr  4621  issref  4622  cnvsym  4623  asymref  4625  intirr  4626  codir  4628  qfto  4629  ssrnres  4678  cnveq0  4692  cnvsn0  4704  dmsnop  4709  rnsnop  4716  resdm2  4726  dfco2a  4736  cocnvcnv1  4746  coi2  4752  coires1  4753  cnvssrndm  4757  cossxp  4758  relrelss  4759  relcoi2  4763  unidmrn  4765  dfdm2  4767  unixpm  4768  cnvexg  4770  cnvex  4771  cnviinm  4774  iotaval  4793  funeqi  4836  funi  4846  funopg  4848  funres  4855  funcnvsn  4859  funcnvcnv  4872  funin  4884  funcnvres  4886  isarep2  4900  fneq1i  4907  fneq2i  4908  fnresdisj  4923  fnresi  4930  mpt0  4940  dmmpti  4942  feq1i  4953  feq2i  4954  fdmi  4965  fun2  4977  fssres  4979  resasplitss  4982  fintm  4988  fconst6  4999  f1ores  5054  foimacnv  5057  resdif  5061  funcocnv2  5064  f1ovi  5078  fveq1i  5092  fveq2i  5094  0fv  5121  fvun1  5152  fvopab3ig  5159  fvmptss2  5160  fndmdif  5185  fneqeql2  5189  f1oresrab  5242  fmptco  5243  fnressn  5262  fressnfv  5263  fmptap  5266  fvsnun1  5273  fvsnun2  5274  fsnunfv  5276  fconst2  5291  mptex  5300  riotabiia  5397  acexmidlema  5415  acexmidlemb  5416  acexmidlemcase  5419  acexmidlem2  5421  acexmidlemv  5422  oveq1i  5434  oveq2i  5435  oveqi  5437  oprabidlem  5448  0neqopab  5461  oprabbii  5471  oprabss  5501  mpt2mpt  5507  funoprab  5512  fnoprab  5515  fovcl  5517  ovigg  5532  elmpt2cl  5609  resfunexgALT  5648  cofunexg  5649  opabex3d  5659  opabex3  5660  1st0  5682  2nd0  5683  op1st  5684  op2nd  5685  fo1st  5695  fo2nd  5696  f1stres  5697  f2ndres  5698  fo1stresm  5699  fo2ndresm  5700  1stcof  5701  2ndcof  5702  1stexg  5705  2ndexg  5706  releldm2  5722  reldm  5723  dfoprab3  5728  mpt2mptsx  5734  mpt2mpts  5735  fnmpt2i  5741  dmmpt2  5742  mpt2exxg  5744  1stconst  5753  2ndconst  5754  dfmpt2  5755  algrflem  5761  mpt2xopn0yelv  5764  mpt2xopoveq  5765  tposssxp  5774  brtpos2  5776  reldmtpos  5778  dftpos2  5786  dftpos4  5788  tpostpos  5789  tpostpos2  5790  tposfo  5796  tposf  5797  tposeqi  5802  tposex  5803  tposoprab  5805  issmo  5813  smores  5817  smores2  5819  iordsmo  5822  smo0  5823  tfrlem8  5844  tfrlemi14  5857  tfrexlem  5858  tfri2  5862  rdgi0g  5874  rdgisuc1  5879  rdg0  5883  frec0g  5890  frecsuclem1  5891  frecsuclem2  5893  frecrdg  5896  2on0  5913  xp01disj  5920  2oconcl  5925  fnoa  5930  oaexg  5931  fnom  5933  omexg  5934  fnoei  5935  oeiexg  5936  oacl  5943  oasuc  5947  o1p1e2  5951  omsuc  5954  nna0r  5960  nnm0r  5961  1onn  5992  2onn  5993  3onn  5994  4onn  5995  eqerlem  6036  elqs  6056  qsex  6062  ecqs  6067  iinerm  6077  th3qlem1  6107  th3q  6110  0npi  6159  dmaddpi  6171  dmmulpi  6172  1lt2pi  6186  0nnq  6209  1nq  6211  dmaddpq  6224  dmmulpq  6225  rec1nq  6240  1lt2nq  6250  halfnqq  6253  prarloclemarch2  6262  enq0enq  6272  nqnq0pi  6279  nnnq0lem1  6287  addnnnq0  6290  mulnnnq0  6291  nq0m0r  6297  prarloclem5  6340  prarloclemcalc  6342  1pr  6390  1idprl  6415  1idpru  6416  ltexprlemm  6423  recexprlem1ssl  6454  recexprlem1ssu  6455  prsrlem1  6480  addsrpr  6483  mulsrpr  6484  gt0srpr  6486  0nsr  6487  0r  6488  1sr  6489  m1r  6490  m1m1sr  6499  addresr  6543  mulresr  6544  axi2m1  6564  axcnre  6570  mulid1i  6630  mulid2i  6631  pnfnre  6667  mnfnre  6668  rexri  6678  ltnri  6710  ltleii  6720  00id  6754  addid1i  6755  addid2i  6756  0cnALT  6801  negeqi  6805  negicn  6812  neg0  6856  renegcli  6872  negcli  6878  negidi  6879  negnegi  6880  subidi  6881  subid1i  6882  negne0bi  6883  negrebi  6884  mul02i  6986  mul01i  6987  mulm1i  6999  leidi  7075  gt0ne0ii  7077  inelr  7171  msqge0i  7204  gt0ap0ii  7213  1div1e1  7266  div1i  7301  eqnegi  7302  recclapi  7303  recidapi  7304  divmulapi  7327  rerecclapi  7338  redivclapi  7340  recgt0  7399  ltp1i  7454  divgt0ii  7468  ltmul1ii  7477  ltdiv1ii  7478  peano5nni  7500  nnrei  7506  1nn  7508  nngt0i  7527  2timesi  7619  times2i  7620  2nn  7656  3nn  7657  4nn  7658  5nn  7659  6nn  7660  7nn  7661  8nn  7662  9nn  7663  10nn  7664  2muline0  7728  rehalfcli  7751  nn0ssre  7759  nnnn0i  7763  dfn2  7768  0nn0  7770  nn0ge0i  7783  zrei  7825  neg1z  7850  nn0negzi  7853  nneoi  7906  peano5uzi  7911  dfuzi  7912  nn0ind-raph  7919  deceq1i  7935  deceq2i  7936  numltc  7950  divfnzn  8038  qdivcl  8058  irrmul  8062  elabf2  8186  bd0  8209  bdeli  8231  bdcriota  8268  bdbm1.3ii  8275  bdinex1  8280  bdssexi  8284  bj-inex  8288  bj-snex  8294  bj-sucex  8304  bj-notbii  8307  bj-d0clsepcl  8310  bj-omind  8318  bj-om  8321  bj-2inf  8322  bj-peano2  8323  bdpeano5  8327  bj-inf2vnlem1  8350  bj-omex2  8357  bj-nn0sucALT  8358
  Copyright terms: Public domain W3C validator