Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-mp GIF 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 wff ψ
 Colors of variables: wff set class This axiom is referenced by:  mp2b  8  a1i  9  mp1i  10  a2i  11  mpd  13  mp2  16  idALT  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  6414  nqnq0pi  6421  nnnq0lem1  6429  addnnnq0  6432  mulnnnq0  6433  nq0m0r  6439  addpinq1  6447  prarloclem5  6483  prarloclemcalc  6485  1pr  6535  1idprl  6566  1idpru  6567  ltexprlemm  6574  recexprlem1ssl  6605  recexprlem1ssu  6606  prsrlem1  6670  addsrpr  6673  mulsrpr  6674  gt0srpr  6676  0nsr  6677  0r  6678  1sr  6679  m1r  6680  m1m1sr  6689  addresr  6734  mulresr  6735  pitonnlem1  6741  axi2m1  6759  axcnre  6765  mulid1i  6827  mulid2i  6828  pnfnre  6864  mnfnre  6865  rexri  6875  ltnri  6907  ltleii  6917  00id  6951  addid1i  6952  addid2i  6953  0cnALT  6998  negeqi  7002  negicn  7009  neg0  7053  renegcli  7069  negcli  7075  negidi  7076  negnegi  7077  subidi  7078  subid1i  7079  negne0bi  7080  negrebi  7081  mul02i  7183  mul01i  7184  mulm1i  7196  leidi  7272  gt0ne0ii  7274  inelr  7368  msqge0i  7401  gt0ap0ii  7410  1div1e1  7463  div1i  7498  eqnegi  7499  recclapi  7500  recidapi  7501  divmulapi  7524  rerecclapi  7535  redivclapi  7537  recgt0  7597  ltp1i  7652  divgt0ii  7666  ltmul1ii  7675  ltdiv1ii  7676  peano5nni  7698  nnrei  7704  1nn  7706  nngt0i  7725  neg1ap0  7804  2timesi  7818  times2i  7819  2nn  7855  3nn  7856  4nn  7857  5nn  7858  6nn  7859  7nn  7860  8nn  7861  9nn  7862  10nn  7863  2muline0  7927  rehalfcli  7950  nn0ssre  7961  nnnn0i  7965  dfn2  7970  0nn0  7972  nn0ge0i  7985  zrei  8027  neg1z  8053  nn0negzi  8056  dfz2  8089  nneoi  8118  peano5uzi  8123  dfuzi  8124  nn0ind-raph  8131  deceq1i  8148  deceq2i  8149  numltc  8163  eluzel2  8254  eluz1i  8256  nn0uz  8283  nnuz  8284  lbzbi  8327  divfnzn  8332  qdivcl  8352  irrmul  8356  cnref1o  8357  mnfxr  8464  pnfnemnf  8467  0ltpnf  8473  mnflt0  8475  0lepnf  8481  xrltnsym  8484  xrlttri3  8488  nltpnft  8500  ngtmnft  8501  xrrebnd  8502  xnegmnf  8512  xneg0  8514  xltnegi  8518  ixxex  8538  iooval2  8554  unirnioo  8612  ioorebasg  8614  elrege0  8615  fzval2  8647  fzen  8677  fzprval  8714  fztpval  8715  uzdisj  8725  ige2m1fz  8742  fz0tp  8751  nn0disj  8765  1fv  8766  4fvwrd4  8767  fzo0ss1  8800  fzo01  8842  fzo12sn  8843  fzo0to2pr  8844  fzo0to3tp  8845  fzo0to42pr  8846  frechashgf1o  8886  0exp0e1  8914  qexpcl  8925  qexpclz  8930  m1expcl2  8931  1exp  8938  sqvali  8986  sqcli  8987  sqeq0i  8988  resqcli  8991  sq1  9000  neg1sqe1  9001  cjexp  9121  re0  9123  im0  9124  re1  9125  im1  9126  cj0  9129  cji  9130  recli  9139  imcli  9140  cjcli  9141  replimi  9142  cjcji  9143  reim0bi  9144  rerebi  9145  cjrebi  9146  recji  9147  imcji  9148  cjmulrcli  9149  cjmulvali  9150  cjmulge0i  9151  renegi  9152  imnegi  9153  cjnegi  9154  addcji  9155  sqrtrval  9209  sqrt0  9213  abs0  9222  absi  9223  elabf2  9256  bd0  9279  bdeli  9301  bdcriota  9338  bdbm1.3ii  9346  bdinex1  9354  bdssexi  9358  bj-inex  9362  bj-snex  9368  bj-sucex  9378  bj-notbii  9381  bj-d0clsepcl  9384  bj-omind  9393  bj-om  9396  bj-2inf  9397  bj-peano2  9398  bdpeano5  9403  bj-omssonALT  9423  bj-inf2vnlem1  9430  bj-omex2  9437  bj-nn0sucALT  9438
 Copyright terms: Public domain W3C validator