ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-mp GIF version

Axiom ax-mp 5
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. "Modus ponens" is short for "modus ponendo ponens", a Latin phrase that means "the mode that by affirming affirms" - remark in [Sanford] p. 39. This rule is similar to the rule of modus tollens mto 651.

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, 30-Sep-1992.)

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  110  simpri  112  biimpi  119  bicomi  131  mpbi  144  mpbir  145  imbi1i  237  a1bi  242  tbt  246  biantru  300  biantrur  301  mp2an  422  pm2.65i  628  notnoti  634  pm2.21i  635  pm2.24ii  636  notbii  657  nbn  688  ori  712  orci  720  olci  721  biorfi  735  imorri  738  dcbii  825  simp1i  990  simp2i  991  simp3i  992  3mix1i  1153  3mix2i  1154  3mix3i  1155  3jaoi  1281  mptru  1340  dfnot  1349  mptnan  1401  mtpor  1403  mtpxor  1404  mpg  1427  19.23h  1474  hbequid  1493  axi12  1494  nfri  1499  spi  1516  19.21  1562  eximii  1581  19.35i  1604  nfn  1636  19.37aiv  1653  19.23  1656  exan  1671  equid  1677  hbae  1696  equvini  1731  equveli  1732  sbid  1747  sbieh  1763  exdistrfor  1772  dveeq2or  1788  ax11v  1799  ax11ev  1800  equs5or  1802  sb4or  1805  sb4bor  1807  nfsb2or  1809  sbequilem  1810  sbequi  1811  speiv  1834  nfsbxy  1915  nfsbxyt  1916  sbco  1941  sbcocom  1943  sbcomxyyz  1945  elsb3  1951  elsb4  1952  sbal1yz  1976  dvelimALT  1985  dvelimfv  1986  dvelimor  1993  eumoi  2032  moani  2069  eqeq1i  2147  eqeq2i  2150  eleq1i  2205  eleq2i  2206  nfcrii  2274  neeq1i  2323  neeq2i  2324  necon3i  2356  rspec  2484  rgen2a  2486  mprg  2489  r19.21  2508  r19.23  2540  raleqi  2630  rexeqi  2631  rabeqif  2677  elv  2690  elexi  2698  ceqsal  2715  vtocl3  2742  vtoclef  2759  vtocle  2760  spcv  2779  spcev  2780  clel3  2820  elabf  2827  elab2  2832  elab3  2836  euxfrdc  2870  reueq  2883  rmoimi2  2887  sbsbc  2913  sbc8g  2916  sbc6  2934  sbcie  2943  sbcrex  2988  csbvarg  3030  csbief  3044  csbie2  3049  sbnfc2  3060  sseli  3093  sselii  3094  sseq1i  3123  sseq2i  3124  difeq1i  3190  difeq2i  3191  uneq1i  3226  uneq2i  3227  ineq1i  3273  ineq2i  3274  ssinss1  3305  difdif2ss  3333  n0ii  3371  ne0ii  3372  vn0  3373  vn0m  3374  abf  3406  disj2  3418  difid  3431  0dif  3434  disjdif  3435  difin0  3436  undif1ss  3437  difdifdirss  3447  rgenm  3465  iftruei  3480  iffalsei  3483  ifbieq2i  3495  ifbieq12i  3497  pweqi  3514  pwid  3525  sneqi  3539  elsn  3543  elpr  3548  elsn2  3559  ralsn  3567  rexsn  3568  eltp  3571  rabrsndc  3591  preq1i  3603  preq2i  3604  prid1  3629  snnz  3642  snm  3643  prnz  3645  prm  3646  tpnz  3648  snsssn  3688  opeq1i  3708  opeq2i  3709  unieqi  3746  unissi  3759  inteqi  3775  intmin2  3797  intab  3800  intsn  3806  iinconstm  3822  iuniin  3823  iinss1  3825  iunxdif2  3861  ssiinf  3862  iinss  3864  iinss2  3865  iinab  3874  iundif2ss  3878  iindif2m  3880  iinin2m  3881  iunxsn  3889  iunxprg  3893  iinpw  3903  sndisj  3925  disjxsn  3927  breqi  3935  breq1i  3936  breq2i  3937  brab1  3975  opabbii  3995  truni  4040  bm1.3ii  4049  a9evsep  4050  ax9vsep  4051  zfnuleu  4052  axnul  4053  ssexi  4066  rabex  4072  elpw2  4082  pwnss  4083  iin0r  4093  intv  4094  pwex  4107  snex  4109  notnotsnex  4111  ord3ex  4114  dtruarb  4115  undifexmid  4117  intid  4146  opnzi  4157  copsexg  4166  opelopabf  4196  epelc  4213  elon  4296  inton  4315  onn0  4322  onm  4323  elsuc  4328  elsuc2  4329  sucid  4339  iunsuc  4342  onordi  4348  ontrci  4349  onelssi  4351  eusvnf  4374  ssonunii  4405  sucex  4415  onssi  4431  onsuci  4432  ordtriexmidlem  4435  ordtriexmidlem2  4436  ordtriexmid  4437  ordtri2orexmid  4438  2ordpr  4439  ontr2exmid  4440  onsucsssucexmid  4442  onsucelsucexmid  4445  regexmidlemm  4447  reg2exmid  4451  onirri  4458  ruALT  4466  onprc  4467  sucon  4468  dtru  4475  0elsucexmid  4480  ordpwsucexmid  4485  ordtri2or2exmid  4486  dcextest  4495  omex  4507  find  4513  omelon  4522  nnoni  4524  limom  4527  nnregexmid  4534  omsinds  4535  xpeq1i  4559  xpeq2i  4560  0nelxp  4567  opthprc  4590  mosubop  4605  releqi  4622  relssi  4630  relin1  4657  relin2  4658  reldif  4659  inopab  4671  difopab  4672  xpiindim  4676  opabbi2dv  4688  ideq  4691  coeq1i  4698  coeq2i  4699  cnveqi  4714  eldm  4736  eldm2  4737  dmeqi  4740  dmv  4755  rneqi  4767  elrnmpti  4792  dmex  4805  rnex  4806  reseq1i  4815  reseq2i  4816  residm  4851  resex  4860  resmpt3  4868  imaeq1i  4878  imaeq2i  4879  elima  4886  imaex  4894  elimasn  4906  args  4908  epini  4910  dfse2  4912  relbrcnv  4919  cotr  4920  issref  4921  cnvsym  4922  asymref  4924  intirr  4925  codir  4927  qfto  4928  ssrnres  4981  cnveq0  4995  cnvsn0  5007  dmsnop  5012  rnsnop  5019  resdm2  5029  dfco2a  5039  cocnvcnv1  5049  coi2  5055  coires1  5056  cnvssrndm  5060  cossxp  5061  cocnvres  5063  relrelss  5065  relcoi2  5069  unidmrn  5071  dfdm2  5073  unixpm  5074  cnvexg  5076  cnvex  5077  cnviinm  5080  iotaval  5099  funeqi  5144  funi  5155  funres  5164  funcnvsn  5168  funcnvcnv  5182  funin  5194  funcnvres  5196  isarep2  5210  fneq1i  5217  fneq2i  5218  fnresdisj  5233  fnresi  5240  mpt0  5250  dmmpti  5252  feq1i  5265  feq2i  5266  fdmi  5280  fun2  5296  fssres  5298  resasplitss  5302  fintm  5308  fconst6  5322  f1ores  5382  foimacnv  5385  resdif  5389  funcocnv2  5392  f1ovi  5406  fveq1i  5422  fveq2i  5424  0fv  5456  fvun1  5487  fvopab3ig  5495  fvmptss2  5496  mptrcl  5503  elfvmptrab1  5515  fndmdif  5525  fneqeql2  5529  f1oresrab  5585  fmptco  5586  fnressn  5606  fressnfv  5607  fmptap  5610  fvsnun1  5617  fvsnun2  5618  fsnunfv  5621  fconst2  5637  mptex  5646  riotabiia  5747  acexmidlema  5765  acexmidlemb  5766  acexmidlemcase  5769  acexmidlem2  5771  acexmidlemv  5772  oveq1i  5784  oveq2i  5785  oveqi  5787  oprabidlem  5802  0neqopab  5816  oprabbii  5826  oprabss  5857  mpompt  5863  funoprab  5871  fnoprab  5874  fovcl  5876  ovigg  5891  elmpocl  5968  resfunexgALT  6008  cofunexg  6009  opabex3d  6019  opabex3  6020  1st0  6042  2nd0  6043  op1st  6044  op2nd  6045  f1stres  6057  f2ndres  6058  fo1stresm  6059  fo2ndresm  6060  1stcof  6061  2ndcof  6062  1stexg  6065  2ndexg  6066  releldm2  6083  reldm  6084  dfoprab3  6089  mpomptsx  6095  mpompts  6096  fnmpoi  6102  dmmpo  6103  mpoexxg  6108  1stconst  6118  2ndconst  6119  dfmpo  6120  algrflem  6126  algrflemg  6127  cnvoprab  6131  f1od2  6132  mpoxopn0yelv  6136  mpoxopoveq  6137  tposssxp  6146  brtpos2  6148  reldmtpos  6150  dftpos2  6158  dftpos4  6160  tpostpos  6161  tpostpos2  6162  tposfo  6168  tposf  6169  tposeqi  6174  tposex  6175  tposoprab  6177  issmo  6185  smores  6189  smores2  6191  iordsmo  6194  smo0  6195  tfrlem8  6215  tfrexlem  6231  tfr1onlem3  6235  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlemres  6246  tfri1dALT  6248  tfri2  6263  rdgisuc1  6281  rdg0  6284  frecfun  6292  frec0g  6294  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecrdg  6305  2on0  6323  xp01disj  6330  2oconcl  6336  fnoa  6343  oaexg  6344  fnom  6346  omexg  6347  fnoei  6348  oeiexg  6349  oei0  6355  oacl  6356  oasuc  6360  o1p1e2  6364  omsuc  6368  nna0r  6374  nnm0r  6375  1onn  6416  2onn  6417  3onn  6418  4onn  6419  eqerlem  6460  elqs  6480  qsex  6486  ecqs  6491  iinerm  6501  th3qlem1  6531  th3q  6534  mapsn  6584  mapsnf1o3  6591  ixpiinm  6618  ixpssmap  6626  brdom  6644  f1dom  6654  enref  6659  dom2  6669  idssen  6671  ssdomg  6672  ensymi  6676  ensn1  6690  fiprc  6709  1domsn  6713  xpcomf1o  6719  xpcomco  6720  dom0  6732  0dom  6733  xpmapenlem  6743  phplem2  6747  php5  6752  snnen2og  6753  1nen2  6755  php5dom  6757  ssfilem  6769  ssfiexmid  6770  domfiexmid  6772  0fin  6778  diffitest  6781  findcard  6782  findcard2  6783  findcard2s  6784  isinfinf  6791  ac6sfi  6792  inffiexmid  6800  unfiexmid  6806  xpfi  6818  fisseneq  6820  ssfirab  6822  en1eqsn  6836  snexxph  6838  sbthlem2  6846  sbthlemi3  6847  sbthlemi6  6850  sbthlem7  6851  fi0  6863  supeq1i  6875  infeq1i  6900  djuexb  6929  djuf1olemr  6939  inresflem  6945  djuinr  6948  updjudhcoinlf  6965  updjudhcoinrg  6966  casefun  6970  caserel  6972  caseinj  6974  caseinl  6976  caseinr  6977  omp1eomlem  6979  endjusym  6981  difinfsn  6985  difinfinf  6986  djuinj  6991  0ct  6992  ctmlemr  6993  ctssdclemn0  6995  ctssdccl  6996  omct  7002  ctfoex  7003  finomni  7012  exmidomni  7014  fodjuomni  7021  nnnninf  7023  ctssexmid  7024  fodjumkv  7034  card0  7044  exmidonfinlem  7049  dju1p1e2  7053  exmidfodomrlemim  7057  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  0npi  7128  dmaddpi  7140  dmmulpi  7141  1lt2pi  7155  0nnq  7179  1nq  7181  dmaddpq  7194  dmmulpq  7195  rec1nq  7210  1lt2nq  7221  halfnqq  7225  prarloclemarch2  7234  enq0enq  7246  nqnq0pi  7253  nnnq0lem1  7261  addnnnq0  7264  mulnnnq0  7265  nq0m0r  7271  addpinq1  7279  prarloclem5  7315  prarloclemcalc  7317  1pr  7369  1idprl  7405  1idpru  7406  ltexprlemm  7415  recexprlem1ssl  7448  recexprlem1ssu  7449  suplocexprlemell  7528  suplocexprlem2b  7529  suplocexprlemmu  7533  suplocexprlemdisj  7535  suplocexprlemloc  7536  suplocexprlemub  7538  suplocexprlemlub  7539  prsrlem1  7557  addsrpr  7560  mulsrpr  7561  gt0srpr  7563  0nsr  7564  0r  7565  1sr  7566  m1r  7567  m1m1sr  7576  caucvgsr  7617  suplocsrlempr  7622  addresr  7652  mulresr  7653  pitonnlem1  7660  peano1nnnn  7667  axi2m1  7690  axcnre  7696  peano5nnnn  7707  axcaucvg  7715  mulid1i  7775  mulid2i  7776  pnfnre  7814  mnfnre  7815  pnfnemnf  7827  mnfxr  7829  rexri  7830  ltnri  7863  ltleii  7873  00id  7910  addid1i  7911  addid2i  7912  0cnALT  7959  negeqi  7963  negicn  7970  neg0  8015  renegcli  8031  negcli  8037  negidi  8038  negnegi  8039  subidi  8040  subid1i  8041  negne0bi  8042  negrebi  8043  mul02i  8159  mul01i  8160  mulm1i  8172  leidi  8254  gt0ne0ii  8256  inelr  8353  msqge0i  8386  gt0ap0ii  8397  1div1e1  8471  div1i  8507  eqnegi  8508  recclapi  8509  recidapi  8510  divmulapi  8533  rerecclapi  8544  redivclapi  8546  recgt0  8615  ltp1i  8670  divgt0ii  8684  ltmul1ii  8693  ltdiv1ii  8694  sup3exmid  8722  peano5nni  8730  nnrei  8736  1nn  8738  nngt0i  8757  neg1ap0  8836  2timesi  8857  times2i  8858  2nn  8888  3nn  8889  4nn  8890  5nn  8891  6nn  8892  7nn  8893  8nn  8894  9nn  8895  2muline0  8952  rehalfcli  8975  nn0ssre  8988  nnnn0i  8992  dfn2  8997  0nn0  8999  nn0ge0i  9011  zrei  9067  neg1z  9093  nn0negzi  9096  dfz2  9130  nneoi  9162  peano5uzi  9167  dfuzi  9168  nn0ind-raph  9175  deceq1i  9195  deceq2i  9196  10nn  9204  numltc  9214  eluzel2  9338  eluz1i  9340  nn0uz  9367  nnuz  9368  infrenegsupex  9396  lbzbi  9415  divfnzn  9420  qdivcl  9442  irrmul  9446  cnref1o  9447  0ltpnf  9575  mnflt0  9577  0lepnf  9583  xrltnsym  9586  xrlttri3  9590  nltpnft  9604  ngtmnft  9607  xrrebnd  9609  xnegmnf  9619  xneg0  9621  xltnegi  9625  xaddmnf1  9638  xaddmnf2  9639  mnfaddpnf  9641  xaddid1  9652  xnn0lenn0nn0  9655  xnn0xadd0  9657  xposdif  9672  ixxex  9689  iooval2  9705  unirnioo  9763  ioorebasg  9765  elrege0  9766  fzval2  9800  fzen  9830  fzprval  9869  fztpval  9870  uzdisj  9880  ige2m1fz  9897  fz01or  9898  fz1ssfz0  9904  fz0tp  9908  nn0disj  9922  1fv  9923  4fvwrd4  9924  fzo0ss1  9958  fzo01  10000  fzo12sn  10001  fzo0to2pr  10002  fzo0to3tp  10003  fzo0to42pr  10004  qbtwnxr  10042  flval  10052  modqfrac  10117  modqmulnn  10122  q2txmodxeq0  10164  frecuzrdgdom  10198  frecuzrdgfun  10200  frecuzrdgsuct  10204  frechashgf1o  10208  nnct  10215  fxnn0nninf  10218  0tonninf  10219  1tonninf  10220  iseqvalcbv  10237  ser0f  10295  0exp0e1  10305  qexpcl  10316  qexpclz  10321  m1expcl2  10322  1exp  10329  sqvali  10379  sqcli  10380  sqeq0i  10381  resqcli  10384  sq1  10393  neg1sqe1  10394  iexpcyc  10404  facnn  10480  fac0  10481  fac1  10482  fac2  10484  fac3  10485  fac4  10486  bcval  10502  bcm1k  10513  bcpasc  10519  bccl  10520  4bc3eq4  10526  4bc2eq6  10527  hashinfom  10531  hashennn  10533  hashfz1  10536  fihasheq0  10547  hash0  10550  hashsng  10551  fihashen1  10552  omgadd  10555  hashp1i  10563  hashxp  10579  fimaxq  10580  zfz1iso  10591  shftidt2  10611  cjexp  10672  re0  10674  im0  10675  re1  10676  im1  10677  cj0  10680  cji  10681  recli  10690  imcli  10691  cjcli  10692  replimi  10693  cjcji  10694  reim0bi  10695  rerebi  10696  cjrebi  10697  recji  10698  imcji  10699  cjmulrcli  10700  cjmulvali  10701  cjmulge0i  10702  renegi  10703  imnegi  10704  cjnegi  10705  addcji  10706  uzin2  10766  rexanuz  10767  rexfiuz  10768  sqrtrval  10779  sqrt0  10783  resqrexlemcalc3  10795  resqrexlemcvg  10798  resqrex  10805  abs0  10837  absi  10838  qabsor  10854  absimle  10863  recan  10888  caubnd2  10896  leabsi  10907  absrei  10908  sqrtpclii  10909  sqrtgt0ii  10910  absvalsqi  10919  absvalsq2i  10920  abscli  10921  absge0i  10922  absval2i  10923  abs00i  10924  absgt0api  10925  absnegi  10926  abscji  10927  releabsi  10928  infxrnegsupex  11039  xrbdtri  11052  cbvsum  11136  sumeq1i  11139  sum0  11164  isumz  11165  fisumss  11168  fsumsersdc  11171  fsumadd  11182  isumclim  11197  isumclim3  11199  fsumcnv  11213  modfsummodlem1  11232  fsumrelem  11247  binomlem  11259  binom  11260  arisum2  11275  expcnv  11280  0.999...  11297  prodf1f  11319  cbvprod  11334  prodeq1i  11337  ef0lem  11373  esum  11375  ere  11383  ege2le3  11384  ef0  11385  eff2  11393  efsep  11404  reeff1  11413  sin0  11442  cos0  11443  ef01bndlem  11469  cos2bnd  11473  sincos1sgn  11477  sincos2sgn  11478  sin4lt0  11479  eirr  11491  0dvds  11519  dvds1  11557  z0even  11614  n2dvdsm1  11616  z2even  11617  n2dvds3  11618  ndvdssub  11633  ndvdsi  11636  flodddiv4  11637  gcddvds  11658  gcd1  11681  6gcd4e2  11689  bezoutlembi  11699  dfgcd3  11704  dfgcd2  11708  lcmval  11750  lcmcllem  11754  lcmledvds  11757  3lcm2e6woprm  11773  qredeu  11784  isprm2lem  11803  isprm3  11805  prm2orodd  11813  sqrt2irr0  11848  pw2dvds  11850  phicl2  11896  phi1  11901  dfphi2  11902  phiprmpw  11904  ennnfonelemp1  11925  ennnfonelem1  11926  ennnfonelemkh  11931  ennnfonelemex  11933  ennnfonelemnn0  11941  ennnfonelemr  11942  exmidunben  11945  ctinfomlemom  11946  ctinfom  11947  ctinf  11949  qnnen  11950  omctfn  11962  omiunct  11963  structcnvcnv  11984  structfun  11986  structfn  11987  ndxarg  11991  ndxid  11992  setsresg  12006  setsslnid  12019  strleun  12057  strle1g  12058  istopon  12189  topontopi  12192  toponunii  12193  toponrestid  12197  istps  12208  topontopn  12213  eltpsi  12217  eltg4i  12233  eltg3  12235  tg1  12237  tg2  12238  tgclb  12243  topnex  12264  sn0topon  12266  distps  12269  cldrcl  12280  sn0cld  12315  restco  12352  lmrcl  12369  ssidcn  12388  cnconst2  12411  cnptopresti  12416  cnptoprest  12417  txuni2  12434  txbas  12436  eltx  12437  txcnp  12449  upxp  12450  txcnmpt  12451  uptx  12452  txcn  12453  txrest  12454  txlm  12457  cnmptid  12459  cnmpt1st  12466  cnmpt2nd  12467  hmeofn  12480  psmetge0  12509  ismeti  12524  xmetunirn  12536  xmetge0  12543  unirnblps  12600  unirnbl  12601  mopnex  12683  qtopbasss  12699  retop  12702  uniretop  12703  iooretopg  12706  cnxmet  12709  cntoptopon  12710  cnbl0  12712  rexmet  12719  blssioo  12723  tgioo  12724  tgqioo  12725  cnopnap  12772  limcresi  12813  dvfvalap  12828  dvidlemap  12838  dvcnp2cntop  12841  dvcoapbr  12849  dvexp2  12854  dvrecap  12855  dveflem  12864  dvef  12865  reeff1o  12871  sin0pilem1  12878  sin0pilem2  12879  pilem3  12880  pigt2lt4  12881  pire  12883  sinhalfpilem  12888  pidiv2halves  12892  cosneghalfpi  12895  cospi  12897  efipi  12898  sin2pi  12900  cos2pi  12901  ef2pi  12902  cosq14gt0  12929  coseq00topi  12932  coseq0negpitopi  12933  sincos4thpi  12937  sincos6thpi  12939  sincos3rdpi  12940  pigt3  12941  cos02pilt1  12948  ioocosf1o  12951  dfrelog  12955  relogf1o  12956  relogcl  12957  relogiso  12968  ex-fl  12990  ex-ceil  12991  ex-exp  12992  ex-fac  12993  ex-gcd  12996  bj-dcdc  13018  bj-stdc  13019  bj-dcst  13020  bj-stst  13021  bj-el2oss1o  13034  elabf2  13042  bd0  13075  bdeli  13097  bdcriota  13134  bdbm1.3ii  13142  bdinex1  13150  bdssexi  13154  bj-inex  13158  bj-snex  13164  bj-sucex  13174  bj-d0clsepcl  13176  bj-omind  13185  bj-om  13188  bj-2inf  13189  bj-peano2  13190  bdpeano5  13194  bj-omssonALT  13214  bj-inf2vnlem1  13221  bj-omex2  13228  bj-nn0sucALT  13229  subctctexmid  13249  nninfall  13257  nninfsellemqall  13264  nninfsellemeqinf  13265  nninfomnilem  13267  nninfomni  13268  exmidsbthrlem  13270  sbthom  13274  isomninnlem  13278  isomninn  13279  cvgcmp2nlemabs  13280  trilpolemisumle  13284  trilpolemeq1  13286  trilpo  13289  apdifflemr  13291  taupi  13295
  Copyright terms: Public domain W3C validator