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  109  simpri  111  biimpi  118  bicomi  130  mpbi  143  mpbir  144  imbi1i  236  a1bi  241  tbt  245  biantru  296  biantrur  297  mp2an  417  pm2.65i  601  notnoti  607  pm2.21i  608  pm2.24ii  609  notbii  627  nbn  648  ori  675  orci  683  olci  684  biorfi  698  imorri  701  simp1i  950  simp2i  951  simp3i  952  3mix1i  1113  3mix2i  1114  3mix3i  1115  3jaoi  1237  trud  1296  dfnot  1305  mptnan  1357  mtpor  1359  mtpxor  1360  mpg  1383  19.23h  1430  hbequid  1449  axi12  1450  nfri  1455  spi  1472  19.21  1518  eximii  1536  19.35i  1559  nfn  1591  19.37aiv  1608  19.23  1611  exan  1626  equid  1632  hbae  1650  equvini  1685  equveli  1686  sbid  1701  sbieh  1717  exdistrfor  1725  dveeq2or  1741  ax11v  1752  ax11ev  1753  equs5or  1755  sb4or  1758  sb4bor  1760  nfsb2or  1762  sbequilem  1763  sbequi  1764  speiv  1787  nfsbxy  1863  nfsbxyt  1864  sbco  1887  sbcocom  1889  sbcomxyyz  1891  elsb3  1897  elsb4  1898  sbal1yz  1922  dvelimALT  1931  dvelimfv  1932  dvelimor  1939  eumoi  1978  moani  2015  eqeq1i  2092  eqeq2i  2095  eleq1i  2150  eleq2i  2151  nfcrii  2218  neeq1i  2266  neeq2i  2267  necon3i  2299  rspec  2423  rgen2a  2425  mprg  2428  r19.21  2445  r19.23  2476  raleqi  2562  rexeqi  2563  rabeqif  2606  elexi  2625  ceqsal  2642  vtocl3  2669  vtoclef  2685  vtocle  2686  spcv  2705  spcev  2706  clel3  2743  elabf  2750  elab2  2754  elab3  2758  euxfrdc  2792  reueq  2803  rmoimi2  2807  sbsbc  2833  sbc8g  2836  sbc6  2854  sbcie  2862  sbcrex  2907  csbvarg  2947  csbief  2961  csbie2  2966  sbnfc2  2977  sseli  3010  sselii  3011  sseq1i  3039  sseq2i  3040  difeq1i  3103  difeq2i  3104  uneq1i  3139  uneq2i  3140  ineq1i  3186  ineq2i  3187  ssinss1  3217  difdif2ss  3245  vn0  3282  vn0m  3283  abf  3314  disj2  3326  difid  3339  0dif  3342  disjdif  3343  difin0  3344  undif1ss  3345  difdifdirss  3354  rgenm  3371  iftruei  3385  iffalsei  3388  ifbieq2i  3400  ifbieq12i  3402  pweqi  3419  pwid  3429  sneqi  3443  elsn  3447  elpr  3452  elsn2  3461  ralsn  3469  rexsn  3470  eltp  3473  rabrsndc  3493  preq1i  3505  preq2i  3506  prid1  3531  snnz  3542  snm  3543  prnz  3545  prm  3546  tpnz  3548  snsssn  3588  opeq1i  3608  opeq2i  3609  unieqi  3646  unissi  3659  inteqi  3675  intmin2  3697  intab  3700  intsn  3706  iinconstm  3722  iuniin  3723  iinss1  3725  iunxdif2  3761  ssiinf  3762  iinss  3764  iinss2  3765  iinab  3774  iundif2ss  3778  iindif2m  3780  iinin2m  3781  iunxsn  3789  iinpw  3798  sndisj  3816  disjxsn  3818  breqi  3826  breq1i  3827  breq2i  3828  brab1  3865  opabbii  3880  truni  3925  bm1.3ii  3935  a9evsep  3936  ax9vsep  3937  zfnuleu  3938  axnul  3939  ssexi  3952  rabex  3958  elpw2  3968  pwnss  3969  iin0r  3979  intv  3980  pwex  3992  snex  3994  notnotsnex  3996  ord3ex  3999  dtruarb  4000  undifexmid  4002  intid  4025  opnzi  4036  copsexg  4045  opelopabf  4075  epelc  4092  elon  4175  inton  4194  onn0  4201  onm  4202  elsuc  4207  elsuc2  4208  sucid  4218  iunsuc  4221  onordi  4227  ontrci  4228  onelssi  4230  eusvnf  4249  ssonunii  4279  sucex  4289  onssi  4305  onsuci  4306  ordtriexmidlem  4309  ordtriexmidlem2  4310  ordtriexmid  4311  ordtri2orexmid  4312  2ordpr  4313  ontr2exmid  4314  onsucsssucexmid  4316  onsucelsucexmid  4319  regexmidlemm  4321  reg2exmid  4325  onirri  4332  ruALT  4340  onprc  4341  sucon  4342  dtru  4349  0elsucexmid  4354  ordpwsucexmid  4359  ordtri2or2exmid  4360  dcextest  4369  omex  4381  find  4387  omelon  4396  nnoni  4398  limom  4401  nnregexmid  4407  omsinds  4408  xpeq1i  4431  xpeq2i  4432  0nelxp  4438  opthprc  4457  mosubop  4472  releqi  4489  relssi  4497  relin1  4523  relin2  4524  reldif  4525  inopab  4536  difopab  4537  xpiindim  4541  opabbi2dv  4553  ideq  4556  coeq1i  4563  coeq2i  4564  cnveqi  4579  eldm  4601  eldm2  4602  dmeqi  4605  dmv  4620  rneqi  4631  elrnmpti  4656  dmex  4667  rnex  4668  reseq1i  4677  reseq2i  4678  residm  4711  resex  4720  resmpt3  4728  imaeq1i  4738  imaeq2i  4739  elima  4746  imaex  4754  elimasn  4766  args  4768  epini  4770  dfse2  4772  relbrcnv  4779  cotr  4780  issref  4781  cnvsym  4782  asymref  4784  intirr  4785  codir  4787  qfto  4788  ssrnres  4839  cnveq0  4853  cnvsn0  4865  dmsnop  4870  rnsnop  4877  resdm2  4887  dfco2a  4897  cocnvcnv1  4907  coi2  4913  coires1  4914  cnvssrndm  4918  cossxp  4919  cocnvres  4921  relrelss  4923  relcoi2  4927  unidmrn  4929  dfdm2  4931  unixpm  4932  cnvexg  4934  cnvex  4935  cnviinm  4938  iotaval  4957  funeqi  5001  funi  5011  funres  5020  funcnvsn  5024  funcnvcnv  5038  funin  5050  funcnvres  5052  isarep2  5066  fneq1i  5073  fneq2i  5074  fnresdisj  5089  fnresi  5096  mpt0  5106  dmmpti  5108  feq1i  5119  feq2i  5120  fdmi  5133  fun2  5148  fssres  5150  resasplitss  5153  fintm  5159  fconst6  5173  f1ores  5231  foimacnv  5234  resdif  5238  funcocnv2  5241  f1ovi  5255  fveq1i  5269  fveq2i  5271  0fv  5302  fvun1  5333  fvopab3ig  5341  fvmptss2  5342  fndmdif  5367  fneqeql2  5371  f1oresrab  5426  fmptco  5427  fnressn  5446  fressnfv  5447  fmptap  5450  fvsnun1  5457  fvsnun2  5458  fsnunfv  5460  fconst2  5475  mptex  5484  riotabiia  5586  acexmidlema  5604  acexmidlemb  5605  acexmidlemcase  5608  acexmidlem2  5610  acexmidlemv  5611  oveq1i  5623  oveq2i  5624  oveqi  5626  oprabidlem  5637  0neqopab  5651  oprabbii  5661  oprabss  5691  mpt2mpt  5697  funoprab  5702  fnoprab  5705  fovcl  5707  ovigg  5722  elmpt2cl  5799  resfunexgALT  5838  cofunexg  5839  opabex3d  5849  opabex3  5850  1st0  5872  2nd0  5873  op1st  5874  op2nd  5875  f1stres  5887  f2ndres  5888  fo1stresm  5889  fo2ndresm  5890  1stcof  5891  2ndcof  5892  1stexg  5895  2ndexg  5896  releldm2  5912  reldm  5913  dfoprab3  5918  mpt2mptsx  5924  mpt2mpts  5925  fnmpt2i  5931  dmmpt2  5932  mpt2exxg  5934  1stconst  5943  2ndconst  5944  dfmpt2  5945  algrflem  5951  algrflemg  5952  cnvoprab  5956  f1od2  5957  mpt2xopn0yelv  5958  mpt2xopoveq  5959  tposssxp  5968  brtpos2  5970  reldmtpos  5972  dftpos2  5980  dftpos4  5982  tpostpos  5983  tpostpos2  5984  tposfo  5990  tposf  5991  tposeqi  5996  tposex  5997  tposoprab  5999  issmo  6007  smores  6011  smores2  6013  iordsmo  6016  smo0  6017  tfrlem8  6037  tfrexlem  6053  tfr1onlem3  6057  tfr1onlemsucaccv  6060  tfr1onlembxssdm  6062  tfr1onlemres  6068  tfri1dALT  6070  tfri2  6085  rdgisuc1  6103  rdg0  6106  frecfun  6114  frec0g  6116  freccllem  6121  frecfcllem  6123  frecsuclem  6125  frecrdg  6127  2on0  6145  xp01disj  6152  2oconcl  6157  fnoa  6162  oaexg  6163  fnom  6165  omexg  6166  fnoei  6167  oeiexg  6168  oei0  6174  oacl  6175  oasuc  6179  o1p1e2  6183  omsuc  6187  nna0r  6193  nnm0r  6194  1onn  6231  2onn  6232  3onn  6233  4onn  6234  eqerlem  6275  elqs  6295  qsex  6301  ecqs  6306  iinerm  6316  th3qlem1  6346  th3q  6349  mapsn  6399  mapsnf1o3  6406  brdom  6419  f1dom  6429  enref  6434  dom2  6444  idssen  6446  ssdomg  6447  ensymi  6451  ensn1  6465  fiprc  6484  1domsn  6487  xpcomf1o  6493  xpcomco  6494  dom0  6506  0dom  6507  xpmapenlem  6517  phplem2  6521  php5  6526  snnen2og  6527  1nen2  6529  php5dom  6531  ssfilem  6543  ssfiexmid  6544  domfiexmid  6546  0fin  6552  diffitest  6555  findcard  6556  findcard2  6557  findcard2s  6558  isinfinf  6565  ac6sfi  6566  inffiexmid  6574  unfiexmid  6580  xpfi  6590  fisseneq  6592  ssfirab  6593  en1eqsn  6606  snexxph  6608  sbthlem2  6611  sbthlemi3  6612  sbthlemi6  6615  sbthlem7  6616  supeq1i  6627  infeq1i  6652  djuf1olemr  6690  inresflem  6696  djuinr  6699  djuun  6704  updjudhcoinlf  6715  updjudhcoinrg  6716  casefun  6720  caserel  6722  caseinj  6724  djuinj  6730  finomni  6740  exmidomniim  6741  exmidomni  6742  fodjuomni  6748  nnnninf  6750  card0  6760  dju1p1e2  6767  exmidfodomrlemim  6771  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  0npi  6816  dmaddpi  6828  dmmulpi  6829  1lt2pi  6843  0nnq  6867  1nq  6869  dmaddpq  6882  dmmulpq  6883  rec1nq  6898  1lt2nq  6909  halfnqq  6913  prarloclemarch2  6922  enq0enq  6934  nqnq0pi  6941  nnnq0lem1  6949  addnnnq0  6952  mulnnnq0  6953  nq0m0r  6959  addpinq1  6967  prarloclem5  7003  prarloclemcalc  7005  1pr  7057  1idprl  7093  1idpru  7094  ltexprlemm  7103  recexprlem1ssl  7136  recexprlem1ssu  7137  prsrlem1  7232  addsrpr  7235  mulsrpr  7236  gt0srpr  7238  0nsr  7239  0r  7240  1sr  7241  m1r  7242  m1m1sr  7251  caucvgsr  7291  addresr  7318  mulresr  7319  pitonnlem1  7326  peano1nnnn  7333  axi2m1  7354  axcnre  7360  peano5nnnn  7371  axcaucvg  7379  mulid1i  7434  mulid2i  7435  pnfnre  7473  mnfnre  7474  pnfnemnf  7486  mnfxr  7488  rexri  7489  ltnri  7521  ltleii  7531  00id  7567  addid1i  7568  addid2i  7569  0cnALT  7616  negeqi  7620  negicn  7627  neg0  7672  renegcli  7688  negcli  7694  negidi  7695  negnegi  7696  subidi  7697  subid1i  7698  negne0bi  7699  negrebi  7700  mul02i  7812  mul01i  7813  mulm1i  7825  leidi  7904  gt0ne0ii  7906  inelr  8002  msqge0i  8035  gt0ap0ii  8045  1div1e1  8110  div1i  8146  eqnegi  8147  recclapi  8148  recidapi  8149  divmulapi  8172  rerecclapi  8183  redivclapi  8185  recgt0  8246  ltp1i  8301  divgt0ii  8315  ltmul1ii  8324  ltdiv1ii  8325  peano5nni  8360  nnrei  8366  1nn  8368  nngt0i  8387  neg1ap0  8466  2timesi  8480  times2i  8481  2nn  8511  3nn  8512  4nn  8513  5nn  8514  6nn  8515  7nn  8516  8nn  8517  9nn  8518  2muline0  8574  rehalfcli  8597  nn0ssre  8610  nnnn0i  8614  dfn2  8619  0nn0  8621  nn0ge0i  8633  zrei  8689  neg1z  8715  nn0negzi  8718  dfz2  8752  nneoi  8783  peano5uzi  8788  dfuzi  8789  nn0ind-raph  8796  deceq1i  8815  deceq2i  8816  10nn  8824  numltc  8834  eluzel2  8956  eluz1i  8958  nn0uz  8985  nnuz  8986  infrenegsupex  9014  lbzbi  9033  divfnzn  9038  qdivcl  9060  irrmul  9064  cnref1o  9065  0ltpnf  9184  mnflt0  9186  0lepnf  9192  xrltnsym  9195  xrlttri3  9199  nltpnft  9211  ngtmnft  9212  xrrebnd  9213  xnegmnf  9223  xneg0  9225  xltnegi  9229  ixxex  9249  iooval2  9265  unirnioo  9323  ioorebasg  9325  elrege0  9326  fzval2  9359  fzen  9389  fzprval  9426  fztpval  9427  uzdisj  9437  ige2m1fz  9454  fz01or  9455  fz0tp  9463  nn0disj  9477  1fv  9478  4fvwrd4  9479  fzo0ss1  9513  fzo01  9555  fzo12sn  9556  fzo0to2pr  9557  fzo0to3tp  9558  fzo0to42pr  9559  qbtwnxr  9597  flval  9607  modqfrac  9672  modqmulnn  9677  q2txmodxeq0  9719  frecuzrdgdom  9753  frecuzrdgfun  9755  frecuzrdgsuct  9759  frechashgf1o  9763  nnct  9770  fxnn0nninf  9772  0tonninf  9773  1tonninf  9774  iseqvalcbv  9789  iser0f  9849  0exp0e1  9859  qexpcl  9870  qexpclz  9875  m1expcl2  9876  1exp  9883  sqvali  9933  sqcli  9934  sqeq0i  9935  resqcli  9938  sq1  9947  neg1sqe1  9948  iexpcyc  9957  facnn  10032  fac0  10033  fac1  10034  fac2  10036  fac3  10037  fac4  10038  bcval  10054  bcm1k  10065  ibcval5  10068  bcpasc  10071  bccl  10072  4bc3eq4  10078  4bc2eq6  10079  hashinfom  10083  hashennn  10085  hashfz1  10088  fihasheq0  10099  hash0  10102  hashsng  10103  fihashen1  10104  omgadd  10107  hashp1i  10115  hashxp  10131  fimaxq  10132  zfz1iso  10143  shftidt2  10163  cjexp  10223  re0  10225  im0  10226  re1  10227  im1  10228  cj0  10231  cji  10232  recli  10241  imcli  10242  cjcli  10243  replimi  10244  cjcji  10245  reim0bi  10246  rerebi  10247  cjrebi  10248  recji  10249  imcji  10250  cjmulrcli  10251  cjmulvali  10252  cjmulge0i  10253  renegi  10254  imnegi  10255  cjnegi  10256  addcji  10257  uzin2  10316  rexanuz  10317  rexfiuz  10318  sqrtrval  10329  sqrt0  10333  resqrexlemcalc3  10345  resqrexlemcvg  10348  resqrex  10355  abs0  10387  absi  10388  qabsor  10404  absimle  10413  recan  10438  caubnd2  10446  leabsi  10457  absrei  10458  sqrtpclii  10459  sqrtgt0ii  10460  absvalsqi  10469  absvalsq2i  10470  abscli  10471  absge0i  10472  absval2i  10473  abs00i  10474  absgt0api  10475  absnegi  10476  abscji  10477  releabsi  10478  cbvsum  10641  sumeq1i  10644  sum0  10668  isumz  10669  fisumss  10672  fisumsers  10675  0dvds  10698  dvds1  10736  z0even  10793  n2dvdsm1  10795  z2even  10796  n2dvds3  10797  ndvdssub  10812  ndvdsi  10815  flodddiv4  10816  gcddvds  10837  gcd1  10860  6gcd4e2  10866  bezoutlembi  10876  dfgcd3  10881  dfgcd2  10885  eucialg  10923  lcmval  10927  lcmcllem  10931  lcmledvds  10934  3lcm2e6woprm  10950  qredeu  10961  isprm2lem  10980  isprm3  10982  prm2orodd  10990  pw2dvds  11026  phicl2  11072  phi1  11077  dfphi2  11078  phiprmpw  11080  ex-fl  11098  ex-ceil  11099  ex-fac  11100  ex-gcd  11103  elabf2  11127  bd0  11160  bdeli  11182  bdcriota  11219  bdbm1.3ii  11227  bdinex1  11235  bdssexi  11239  bj-inex  11243  bj-snex  11249  bj-sucex  11259  bj-notbii  11262  bj-d0clsepcl  11265  bj-omind  11274  bj-om  11277  bj-2inf  11278  bj-peano2  11279  bdpeano5  11283  bj-omssonALT  11303  bj-inf2vnlem1  11310  bj-omex2  11317  bj-nn0sucALT  11318  nninfall  11345  nninfsellemqall  11352  nninfsellemeqinf  11353  nninfomnilem  11355  nninfomni  11356  exmidsbthrlem  11357
  Copyright terms: Public domain W3C validator