ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-mp 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  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
StepHypRef Expression
1 wps 1  wff  ps
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  108  simpri  110  biimpi  117  bicomi  127  mpbi  137  mpbir  138  imbi1i  231  a1bi  236  tbt  240  biantru  290  biantrur  291  mp2an  410  pm2.65i  578  notnoti  584  pm2.21i  585  pm2.24ii  586  notbii  604  nbn  625  ori  652  orci  660  olci  661  biorfi  675  imorri  678  simp1i  924  simp2i  925  simp3i  926  3mix1i  1087  3mix2i  1088  3mix3i  1089  3jaoi  1209  trud  1268  dfnot  1278  mptnan  1330  mtpor  1332  mtpxor  1333  mpg  1356  19.23h  1403  hbequid  1422  axi12  1423  nfri  1428  spi  1445  19.21  1491  eximii  1509  19.35i  1532  nfn  1564  19.37aiv  1581  19.23  1584  exan  1599  equid  1605  hbae  1622  equvini  1657  equveli  1658  sbid  1673  sbieh  1689  exdistrfor  1697  dveeq2or  1713  ax11v  1724  ax11ev  1725  equs5or  1727  sb4or  1730  sb4bor  1732  nfsb2or  1734  sbequilem  1735  sbequi  1736  speiv  1758  nfsbxy  1834  nfsbxyt  1835  sbco  1858  sbcocom  1860  sbcomxyyz  1862  elsb3  1868  elsb4  1869  sbal1yz  1893  dvelimALT  1902  dvelimfv  1903  dvelimor  1910  eumoi  1949  moani  1986  eqeq1i  2063  eqeq2i  2066  eleq1i  2119  eleq2i  2120  nfcrii  2187  neeq1i  2235  neeq2i  2236  necon3i  2268  rspec  2390  rgen2a  2392  mprg  2395  r19.21  2412  r19.23  2441  raleqi  2526  rexeqi  2527  elexi  2584  ceqsal  2600  vtocl3  2627  vtoclef  2643  vtocle  2644  spcv  2663  spcev  2664  clel3  2701  elabf  2708  elab2  2712  elab3  2716  euxfrdc  2749  reueq  2760  rmoimi2  2764  sbsbc  2790  sbc8g  2793  sbc6  2811  sbcie  2819  sbcrex  2864  csbvarg  2904  csbief  2918  csbie2  2922  sbnfc2  2933  sseli  2968  sselii  2969  sseq1i  2996  sseq2i  2997  psseq1i  3060  psseq2i  3061  difeq1i  3085  difeq2i  3086  uneq1i  3120  uneq2i  3121  ineq1i  3161  ineq2i  3162  ssinss1  3192  difdif2ss  3221  vn0  3258  vn0m  3259  abf  3287  npss0  3293  disj2  3302  difid  3319  0dif  3322  disjdif  3323  difin0  3324  undif1ss  3325  difdifdirss  3334  rgenm  3350  iftruei  3364  iffalsei  3367  ifbieq2i  3378  ifbieq12i  3380  pweqi  3390  pwid  3400  sneqi  3414  elsn  3418  elpr  3423  elsn2  3432  ralsn  3441  rexsn  3442  eltp  3445  r19.12sn  3463  rabrsndc  3465  preq1i  3477  preq2i  3478  prid1  3503  snnz  3514  snm  3515  prnz  3517  prm  3518  tpnz  3520  snsssn  3559  opeq1i  3579  opeq2i  3580  unieqi  3617  unissi  3630  inteqi  3646  intmin2  3668  intab  3671  intsn  3677  iinconstm  3693  iuniin  3694  iinss1  3696  iunxdif2  3732  ssiinf  3733  iinss  3735  iinss2  3736  iinab  3745  iundif2ss  3749  iindif2m  3751  iinin2m  3752  iunxsn  3760  iinpw  3769  sndisj  3787  disjxsn  3789  breqi  3797  breq1i  3798  breq2i  3799  brab1  3836  opabbii  3851  truni  3895  bm1.3ii  3905  a9evsep  3906  ax9vsep  3907  zfnuleu  3908  axnul  3909  ssexi  3922  rabex  3928  elpw2  3938  pwnss  3939  iin0r  3949  intv  3950  snex  3964  ord3ex  3968  dtruarb  3969  snelpw  3976  rext  3978  sspwb  3979  intid  3987  euabex  3988  mss  3989  exss  3990  opi1  3996  opnzi  3999  copsexg  4008  opeqsn  4016  opeqpr  4017  uniop  4019  opelopabf  4038  epelc  4055  elon  4138  inton  4157  onn0  4164  onm  4165  elsuc  4170  elsuc2  4171  sucid  4181  iunsuc  4184  onordi  4190  ontrci  4191  onelssi  4193  snnex  4208  eusvnf  4212  op1stb  4236  ssonunii  4242  sucex  4252  onssi  4268  onsuci  4269  ordtriexmidlem  4272  ordtriexmidlem2  4273  ordtriexmid  4274  ordtri2orexmid  4275  2ordpr  4276  ontr2exmid  4277  onsucsssucexmid  4279  onsucelsucexmid  4282  regexmidlemm  4284  reg2exmid  4288  ruALT  4302  onprc  4303  sucon  4304  dtruex  4310  dtru  4311  0elsucexmid  4316  ordpwsucexmid  4321  ordtri2or2exmid  4323  omex  4343  find  4349  omelon  4358  nnoni  4360  limom  4363  nnregexmid  4369  xpeq1i  4392  xpeq2i  4393  0nelxp  4399  opthprc  4418  mosubop  4433  releqi  4450  relssi  4458  relin1  4482  relin2  4483  reldif  4484  inopab  4495  difopab  4496  xpiindim  4500  opabbi2dv  4512  relop  4513  ideq  4515  coeq1i  4522  coeq2i  4523  cnveqi  4537  eldm  4559  eldm2  4560  dmeqi  4563  dmv  4578  rneqi  4589  elrnmpti  4614  dmex  4625  rnex  4626  reseq1i  4635  reseq2i  4636  residm  4669  resex  4678  resmpt3  4684  imaeq1i  4692  imaeq2i  4693  elima  4700  elimasn  4719  args  4721  epini  4723  dfse2  4725  relbrcnv  4732  cotr  4733  issref  4734  cnvsym  4735  asymref  4737  intirr  4738  codir  4740  qfto  4741  ssrnres  4790  cnveq0  4804  cnvsn0  4816  dmsnop  4821  rnsnop  4828  resdm2  4838  dfco2a  4848  cocnvcnv1  4858  coi2  4864  coires1  4865  cnvssrndm  4869  cossxp  4870  relrelss  4871  relcoi2  4875  unidmrn  4877  dfdm2  4879  unixpm  4880  cnvexg  4882  cnvex  4883  cnviinm  4886  iotaval  4905  funeqi  4949  funi  4959  funopg  4961  funres  4968  funcnvsn  4972  funcnvcnv  4985  funin  4997  funcnvres  4999  isarep2  5013  fneq1i  5020  fneq2i  5021  fnresdisj  5036  fnresi  5043  mpt0  5053  dmmpti  5055  feq1i  5066  feq2i  5067  fdmi  5078  fun2  5091  fssres  5093  resasplitss  5096  fintm  5102  fconst6  5113  f1ores  5168  foimacnv  5171  resdif  5175  funcocnv2  5178  f1ovi  5192  fveq1i  5206  fveq2i  5208  0fv  5235  fvun1  5266  fvopab3ig  5273  fvmptss2  5274  fndmdif  5299  fneqeql2  5303  f1oresrab  5356  fmptco  5357  fnressn  5376  fressnfv  5377  fmptap  5380  fvsnun1  5387  fvsnun2  5388  fsnunfv  5390  fconst2  5405  mptex  5414  riotabiia  5512  acexmidlema  5530  acexmidlemb  5531  acexmidlemcase  5534  acexmidlem2  5536  acexmidlemv  5537  oveq1i  5549  oveq2i  5550  oveqi  5552  oprabidlem  5563  0neqopab  5577  oprabbii  5587  oprabss  5617  mpt2mpt  5623  funoprab  5628  fnoprab  5631  fovcl  5633  ovigg  5648  elmpt2cl  5725  resfunexgALT  5764  cofunexg  5765  opabex3d  5775  opabex3  5776  1st0  5798  2nd0  5799  op1st  5800  op2nd  5801  fo1st  5811  fo2nd  5812  f1stres  5813  f2ndres  5814  fo1stresm  5815  fo2ndresm  5816  1stcof  5817  2ndcof  5818  1stexg  5821  2ndexg  5822  releldm2  5838  reldm  5839  dfoprab3  5844  mpt2mptsx  5850  mpt2mpts  5851  fnmpt2i  5857  dmmpt2  5858  mpt2exxg  5860  1stconst  5869  2ndconst  5870  dfmpt2  5871  algrflem  5877  algrflemg  5878  cnvoprab  5882  f1od2  5883  mpt2xopn0yelv  5884  mpt2xopoveq  5885  tposssxp  5894  brtpos2  5896  reldmtpos  5898  dftpos2  5906  dftpos4  5908  tpostpos  5909  tpostpos2  5910  tposfo  5916  tposf  5917  tposeqi  5922  tposex  5923  tposoprab  5925  issmo  5933  smores  5937  smores2  5939  iordsmo  5942  smo0  5943  tfrlem8  5964  tfrexlem  5978  tfri2  5982  rdgisuc1  6001  rdg0  6004  frec0g  6013  frecsuclem1  6017  frecsuclem2  6019  frecrdg  6022  2on0  6040  xp01disj  6047  2oconcl  6052  fnoa  6057  oaexg  6058  fnom  6060  omexg  6061  fnoei  6062  oeiexg  6063  oei0  6069  oacl  6070  oasuc  6074  o1p1e2  6078  omsuc  6081  nna0r  6087  nnm0r  6088  1onn  6123  2onn  6124  3onn  6125  4onn  6126  eqerlem  6167  elqs  6187  qsex  6193  ecqs  6198  iinerm  6208  th3qlem1  6238  th3q  6241  brdom  6261  f1dom  6270  enref  6275  dom2  6285  idssen  6287  ssdomg  6288  ensymi  6292  ensn1  6306  fiprc  6322  xpcomf1o  6329  xpcomco  6330  phplem2  6346  php5  6351  snnen2og  6352  php5dom  6355  ssfiexmid  6366  0fin  6371  diffitest  6374  findcard  6375  findcard2  6376  findcard2s  6377  ac6sfi  6382  supeq1i  6393  card0  6425  0npi  6468  dmaddpi  6480  dmmulpi  6481  1lt2pi  6495  0nnq  6519  1nq  6521  dmaddpq  6534  dmmulpq  6535  rec1nq  6550  1lt2nq  6561  halfnqq  6565  prarloclemarch2  6574  enq0enq  6586  nqnq0pi  6593  nnnq0lem1  6601  addnnnq0  6604  mulnnnq0  6605  nq0m0r  6611  addpinq1  6619  prarloclem5  6655  prarloclemcalc  6657  1pr  6709  1idprl  6745  1idpru  6746  ltexprlemm  6755  recexprlem1ssl  6788  recexprlem1ssu  6789  prsrlem1  6884  addsrpr  6887  mulsrpr  6888  gt0srpr  6890  0nsr  6891  0r  6892  1sr  6893  m1r  6894  m1m1sr  6903  caucvgsr  6943  addresr  6970  mulresr  6971  pitonnlem1  6978  peano1nnnn  6985  axi2m1  7006  axcnre  7012  peano5nnnn  7023  axcaucvg  7031  mulid1i  7086  mulid2i  7087  pnfnre  7125  mnfnre  7126  rexri  7136  ltnri  7168  ltleii  7178  00id  7214  addid1i  7215  addid2i  7216  0cnALT  7263  negeqi  7267  negicn  7274  neg0  7319  renegcli  7335  negcli  7341  negidi  7342  negnegi  7343  subidi  7344  subid1i  7345  negne0bi  7346  negrebi  7347  mul02i  7458  mul01i  7459  mulm1i  7471  leidi  7550  gt0ne0ii  7552  inelr  7648  msqge0i  7681  gt0ap0ii  7691  1div1e1  7754  div1i  7790  eqnegi  7791  recclapi  7792  recidapi  7793  divmulapi  7816  rerecclapi  7827  redivclapi  7829  recgt0  7890  ltp1i  7945  divgt0ii  7959  ltmul1ii  7968  ltdiv1ii  7969  peano5nni  7992  nnrei  7998  1nn  8000  nngt0i  8019  neg1ap0  8098  2timesi  8112  times2i  8113  2nn  8143  3nn  8144  4nn  8145  5nn  8146  6nn  8147  7nn  8148  8nn  8149  9nn  8150  2muline0  8206  rehalfcli  8229  nn0ssre  8242  nnnn0i  8246  dfn2  8251  0nn0  8253  nn0ge0i  8265  zrei  8307  neg1z  8333  nn0negzi  8336  dfz2  8370  nneoi  8400  peano5uzi  8405  dfuzi  8406  nn0ind-raph  8413  deceq1i  8432  deceq2i  8433  10nn  8441  numltc  8451  eluzel2  8573  eluz1i  8575  nn0uz  8602  nnuz  8603  lbzbi  8647  divfnzn  8652  qdivcl  8674  irrmul  8678  cnref1o  8679  mnfxr  8794  pnfnemnf  8797  0ltpnf  8803  mnflt0  8805  0lepnf  8811  xrltnsym  8814  xrlttri3  8818  nltpnft  8830  ngtmnft  8831  xrrebnd  8832  xnegmnf  8842  xneg0  8844  xltnegi  8848  ixxex  8868  iooval2  8884  unirnioo  8942  ioorebasg  8944  elrege0  8945  fzval2  8978  fzen  9008  fzprval  9045  fztpval  9046  uzdisj  9056  ige2m1fz  9073  fz0tp  9082  nn0disj  9096  1fv  9097  4fvwrd4  9098  fzo0ss1  9131  fzo01  9173  fzo12sn  9174  fzo0to2pr  9175  fzo0to3tp  9176  fzo0to42pr  9177  qbtwnxr  9213  flval  9223  modqfrac  9286  modqmulnn  9291  q2txmodxeq0  9333  frechashgf1o  9368  iser0f  9415  0exp0e1  9424  qexpcl  9435  qexpclz  9440  m1expcl2  9441  1exp  9448  sqvali  9498  sqcli  9499  sqeq0i  9500  resqcli  9503  sq1  9512  neg1sqe1  9513  iexpcyc  9522  facnn  9594  fac0  9595  fac1  9596  fac2  9598  fac3  9599  fac4  9600  bcval  9616  bcm1k  9627  ibcval5  9630  bcpasc  9633  bccl  9634  4bc3eq4  9640  4bc2eq6  9641  shftidt2  9660  cjexp  9720  re0  9722  im0  9723  re1  9724  im1  9725  cj0  9728  cji  9729  recli  9738  imcli  9739  cjcli  9740  replimi  9741  cjcji  9742  reim0bi  9743  rerebi  9744  cjrebi  9745  recji  9746  imcji  9747  cjmulrcli  9748  cjmulvali  9749  cjmulge0i  9750  renegi  9751  imnegi  9752  cjnegi  9753  addcji  9754  uzin2  9813  rexanuz  9814  rexfiuz  9815  sqrtrval  9826  sqrt0  9830  resqrexlemcalc3  9842  resqrexlemcvg  9845  resqrex  9852  abs0  9884  absi  9885  qabsor  9901  absimle  9910  recan  9935  caubnd2  9943  leabsi  9954  absrei  9955  sqrtpclii  9956  sqrtgt0ii  9957  absvalsqi  9966  absvalsq2i  9967  abscli  9968  absge0i  9969  absval2i  9970  abs00i  9971  absgt0api  9972  absnegi  9973  abscji  9974  releabsi  9975  0dvds  10127  dvds1  10164  fz01or  10189  z0even  10222  n2dvdsm1  10224  z2even  10225  n2dvds3  10226  pw2dvds  10233  ex-fl  10258  ex-ceil  10259  ex-fac  10260  elabf2  10287  bd0  10310  bdeli  10332  bdcriota  10369  bdbm1.3ii  10377  bdinex1  10385  bdssexi  10389  bj-inex  10393  bj-snex  10399  bj-sucex  10409  bj-notbii  10412  bj-d0clsepcl  10415  bj-omind  10424  bj-om  10427  bj-2inf  10428  bj-peano2  10429  bdpeano5  10434  bj-omssonALT  10454  bj-inf2vnlem1  10461  bj-omex2  10468  bj-nn0sucALT  10469
  Copyright terms: Public domain W3C validator