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  404  pm2.65i  555  notnoti  561  pm2.21i  562  pm2.24ii  563  notbii  581  nbn  602  ori  629  orci  637  olci  638  biorfi  652  imorri  655  simp1i  899  simp2i  900  simp3i  901  3mix1i  1062  3mix2i  1063  3mix3i  1064  3jaoi  1182  trud  1235  dfnot  1245  mpto1  1295  mtp-xor  1297  mtp-or  1298  mpg  1316  19.23h  1364  hbequid  1383  axi12  1384  nfri  1389  equidqeOLD  1403  spi  1407  19.21  1453  eximii  1471  19.35i  1494  nfn  1526  19.37aiv  1543  19.23  1546  exan  1561  equid  1567  hbae  1584  equvini  1619  equveli  1620  sbid  1635  sbieh  1651  exdistrfor  1659  dveeq2or  1675  ax11v  1686  ax11ev  1687  equs5or  1689  sb4or  1692  sb4bor  1694  nfsb2or  1696  sbequilem  1697  sbequi  1698  speiv  1720  nfsbxy  1796  nfsbxyt  1797  sbco  1820  sbcocom  1822  sbcomxyyz  1824  elsb3  1830  elsb4  1831  sbal1yz  1855  dvelimALT  1864  dvelimfv  1865  dvelimor  1872  eumoi  1911  moani  1948  eqeq1i  2025  eqeq2i  2028  eleq1i  2081  eleq2i  2082  nfcrii  2149  neeq1i  2195  neeq2i  2196  necon3i  2227  rspec  2347  rgen2a  2349  mprg  2352  r19.21  2369  r19.23  2398  raleqi  2483  rexeqi  2484  elexi  2540  ceqsal  2556  vtocl3  2583  vtoclef  2599  vtocle  2600  spcv  2619  spcev  2620  clel3  2652  elabf  2659  elab2  2663  elab3  2667  euxfrdc  2700  reueq  2711  rmoimi2  2715  sbsbc  2741  sbc8g  2744  sbc6  2762  sbcie  2770  csbvarg  2850  csbief  2864  csbie2  2868  sbnfc2  2879  sseli  2914  sselii  2915  sseq1i  2942  sseq2i  2943  psseq1i  3006  psseq2i  3007  difeq1i  3031  difeq2i  3032  uneq1i  3066  uneq2i  3067  ineq1i  3107  ineq2i  3108  ssinss1  3138  difdif2ss  3167  vn0  3204  vn0m  3205  abf  3233  npss0  3239  disj2  3248  difid  3265  0dif  3268  disjdif  3269  difin0  3270  undif1ss  3271  difdifdirss  3280  rgenm  3298  iftruei  3312  iffalsei  3314  ifbieq2i  3324  ifbieq12i  3326  pweqi  3334  pwid  3344  sneqi  3358  elpr  3364  elsnc  3369  elsnc2  3376  ralsn  3384  rexsn  3385  eltp  3388  r19.12sn  3406  rabrsndc  3408  preq1i  3420  preq2i  3421  prid1  3446  snnz  3457  snm  3458  prnz  3460  prm  3461  tpnz  3463  snsssn  3502  opeq1i  3522  opeq2i  3523  unieqi  3560  unissi  3573  inteqi  3589  intmin2  3611  intab  3614  intsn  3620  iinconstm  3636  iuniin  3637  iinss1  3639  iunxdif2  3675  ssiinf  3676  iinss  3678  iinss2  3679  iinab  3688  iundif2ss  3692  iindif2m  3694  iinin2m  3695  iunxsn  3703  iinpw  3712  sndisj  3730  disjxsn  3732  breqi  3740  breq1i  3741  breq2i  3742  brab1  3779  opabbii  3794  truni  3838  bm1.3ii  3848  a9evsep  3849  ax9vsep  3850  zfnuleu  3851  axnul  3852  ssexi  3865  rabex  3871  elpw2  3881  pwnss  3882  iin0r  3892  intv  3893  snex  3907  ord3ex  3911  dtruarb  3912  snelpw  3919  rext  3921  sspwb  3922  intid  3930  euabex  3931  mss  3932  exss  3933  opi1  3939  opnzi  3942  copsexg  3951  opeqsn  3959  opeqpr  3960  uniop  3962  opelopabf  3981  epelc  3998  elon  4056  inton  4075  onn0  4082  onm  4083  elsuc  4088  elsuc2  4089  sucid  4099  iunsuc  4102  onordi  4109  ontrci  4110  onelssi  4112  snnex  4127  eusvnf  4131  op1stb  4155  ssonunii  4161  sucex  4171  onssi  4186  onsuci  4187  ordtriexmidlem  4188  ordtriexmidlem2  4189  ordtriexmid  4190  ordtri2orexmid  4191  onsucsssucexmid  4192  onsucelsucexmidlem  4194  onsucelsucexmid  4195  regexmidlemm  4197  ruALT  4209  onprc  4210  sucon  4211  dtruex  4217  dtru  4218  ordpwsucexmid  4226  omex  4239  find  4245  omelon  4254  nnoni  4256  limom  4259  nnregexmid  4265  xpeq1i  4288  xpeq2i  4289  0nelxp  4295  opthprc  4314  mosubop  4329  releqi  4346  relssi  4354  relin1  4378  relin2  4379  reldif  4380  inopab  4391  difopab  4392  xpiindim  4396  opabbi2dv  4408  relop  4409  ideq  4411  coeq1i  4418  coeq2i  4419  cnveqi  4433  eldm  4455  eldm2  4456  dmeqi  4459  dmv  4474  rneqi  4485  elrnmpti  4510  dmex  4521  rnex  4522  reseq1i  4531  reseq2i  4532  residm  4565  resex  4574  resmpt3  4580  imaeq1i  4588  imaeq2i  4589  elima  4596  elimasn  4615  args  4617  epini  4619  dfse2  4621  relbrcnv  4628  cotr  4629  issref  4630  cnvsym  4631  asymref  4633  intirr  4634  codir  4636  qfto  4637  ssrnres  4686  cnveq0  4700  cnvsn0  4712  dmsnop  4717  rnsnop  4724  resdm2  4734  dfco2a  4744  cocnvcnv1  4754  coi2  4760  coires1  4761  cnvssrndm  4765  cossxp  4766  relrelss  4767  relcoi2  4771  unidmrn  4773  dfdm2  4775  unixpm  4776  cnvexg  4778  cnvex  4779  cnviinm  4782  iotaval  4801  funeqi  4844  funi  4854  funopg  4856  funres  4863  funcnvsn  4867  funcnvcnv  4880  funin  4892  funcnvres  4894  isarep2  4908  fneq1i  4915  fneq2i  4916  fnresdisj  4931  fnresi  4938  mpt0  4948  dmmpti  4950  feq1i  4961  feq2i  4962  fdmi  4973  fun2  4985  fssres  4987  resasplitss  4990  fintm  4996  fconst6  5007  f1ores  5062  foimacnv  5065  resdif  5069  funcocnv2  5072  f1ovi  5086  fveq1i  5100  fveq2i  5102  0fv  5129  fvun1  5160  fvopab3ig  5167  fvmptss2  5168  fndmdif  5193  fneqeql2  5197  f1oresrab  5250  fmptco  5251  fnressn  5270  fressnfv  5271  fmptap  5274  fvsnun1  5281  fvsnun2  5282  fsnunfv  5284  fconst2  5299  mptex  5308  riotabiia  5405  acexmidlema  5423  acexmidlemb  5424  acexmidlemcase  5427  acexmidlem2  5429  acexmidlemv  5430  oveq1i  5442  oveq2i  5443  oveqi  5445  oprabidlem  5456  0neqopab  5469  oprabbii  5479  oprabss  5509  mpt2mpt  5515  funoprab  5520  fnoprab  5523  fovcl  5525  ovigg  5540  elmpt2cl  5617  resfunexgALT  5656  cofunexg  5657  opabex3d  5667  opabex3  5668  1st0  5690  2nd0  5691  op1st  5692  op2nd  5693  fo1st  5703  fo2nd  5704  f1stres  5705  f2ndres  5706  fo1stresm  5707  fo2ndresm  5708  1stcof  5709  2ndcof  5710  1stexg  5713  2ndexg  5714  releldm2  5730  reldm  5731  dfoprab3  5736  mpt2mptsx  5742  mpt2mpts  5743  fnmpt2i  5749  dmmpt2  5750  mpt2exxg  5752  1stconst  5761  2ndconst  5762  dfmpt2  5763  algrflem  5769  mpt2xopn0yelv  5772  mpt2xopoveq  5773  tposssxp  5782  brtpos2  5784  reldmtpos  5786  dftpos2  5794  dftpos4  5796  tpostpos  5797  tpostpos2  5798  tposfo  5804  tposf  5805  tposeqi  5810  tposex  5811  tposoprab  5813  issmo  5821  smores  5825  smores2  5827  iordsmo  5830  smo0  5831  tfrlem8  5852  tfrlemi14  5865  tfrexlem  5866  tfri2  5870  rdgi0g  5882  rdgisuc1  5887  rdg0  5891  frec0g  5898  frecsuclem1  5899  frecsuclem2  5901  frecrdg  5904  2on0  5921  xp01disj  5928  2oconcl  5933  fnoa  5938  oaexg  5939  fnom  5941  omexg  5942  fnoei  5943  oeiexg  5944  oacl  5951  oasuc  5955  o1p1e2  5959  omsuc  5962  nna0r  5968  nnm0r  5969  1onn  6000  2onn  6001  3onn  6002  4onn  6003  eqerlem  6044  elqs  6064  qsex  6070  ecqs  6075  iinerm  6085  th3qlem1  6115  th3q  6118  0npi  6167  dmaddpi  6179  dmmulpi  6180  1lt2pi  6194  0nnq  6217  1nq  6219  dmaddpq  6232  dmmulpq  6233  rec1nq  6248  1lt2nq  6258  halfnqq  6261  prarloclemarch2  6270  enq0enq  6280  nqnq0pi  6287  nnnq0lem1  6295  addnnnq0  6298  mulnnnq0  6299  nq0m0r  6305  prarloclem5  6348  prarloclemcalc  6350  1pr  6398  1idprl  6423  1idpru  6424  ltexprlemm  6431  recexprlem1ssl  6461  recexprlem1ssu  6462  prsrlem1  6486  addsrpr  6489  mulsrpr  6490  gt0srpr  6492  0nsr  6493  0r  6494  1sr  6495  m1r  6496  m1m1sr  6505  addresr  6547  mulresr  6548  axi2m1  6568  axcnre  6574  mulid1i  6632  mulid2i  6633  pnfnre  6669  mnfnre  6670  rexri  6680  ltnri  6712  ltleii  6722  00id  6756  addid1i  6757  addid2i  6758  0cnALT  6803  negeqi  6807  negicn  6814  neg0  6858  renegcli  6874  negcli  6880  negidi  6881  negnegi  6882  subidi  6883  subid1i  6884  negne0bi  6885  negrebi  6886  mul02i  6988  mul01i  6989  mulm1i  7001  leidi  7077  gt0ne0ii  7079  inelr  7173  elabf2  7220  bd0  7243  bdeli  7265  bdcriota  7302  bdbm1.3ii  7309  bdinex1  7314  bdssexi  7318  bj-inex  7322  bj-snex  7328  bj-sucex  7338  bj-notbii  7341  bj-d0clsepcl  7344  bj-omind  7352  bj-om  7355  bj-2inf  7356  bj-peano2  7357  bdpeano5  7361  bj-inf2vnlem1  7384  bj-omex2  7391  bj-nn0sucALT  7392
  Copyright terms: Public domain W3C validator