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 636.

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  613  notnoti  619  pm2.21i  620  pm2.24ii  621  notbii  642  nbn  673  ori  697  orci  705  olci  706  biorfi  720  imorri  723  dcbii  810  simp1i  975  simp2i  976  simp3i  977  3mix1i  1138  3mix2i  1139  3mix3i  1140  3jaoi  1266  mptru  1325  dfnot  1334  mptnan  1386  mtpor  1388  mtpxor  1389  mpg  1412  19.23h  1459  hbequid  1478  axi12  1479  nfri  1484  spi  1501  19.21  1547  eximii  1566  19.35i  1589  nfn  1621  19.37aiv  1638  19.23  1641  exan  1656  equid  1662  hbae  1681  equvini  1716  equveli  1717  sbid  1732  sbieh  1748  exdistrfor  1756  dveeq2or  1772  ax11v  1783  ax11ev  1784  equs5or  1786  sb4or  1789  sb4bor  1791  nfsb2or  1793  sbequilem  1794  sbequi  1795  speiv  1818  nfsbxy  1895  nfsbxyt  1896  sbco  1919  sbcocom  1921  sbcomxyyz  1923  elsb3  1929  elsb4  1930  sbal1yz  1954  dvelimALT  1963  dvelimfv  1964  dvelimor  1971  eumoi  2010  moani  2047  eqeq1i  2125  eqeq2i  2128  eleq1i  2183  eleq2i  2184  nfcrii  2251  neeq1i  2300  neeq2i  2301  necon3i  2333  rspec  2461  rgen2a  2463  mprg  2466  r19.21  2485  r19.23  2517  raleqi  2607  rexeqi  2608  rabeqif  2651  elv  2664  elexi  2672  ceqsal  2689  vtocl3  2716  vtoclef  2733  vtocle  2734  spcv  2753  spcev  2754  clel3  2794  elabf  2801  elab2  2805  elab3  2809  euxfrdc  2843  reueq  2856  rmoimi2  2860  sbsbc  2886  sbc8g  2889  sbc6  2907  sbcie  2915  sbcrex  2960  csbvarg  3000  csbief  3014  csbie2  3019  sbnfc2  3030  sseli  3063  sselii  3064  sseq1i  3093  sseq2i  3094  difeq1i  3160  difeq2i  3161  uneq1i  3196  uneq2i  3197  ineq1i  3243  ineq2i  3244  ssinss1  3275  difdif2ss  3303  n0ii  3341  ne0ii  3342  vn0  3343  vn0m  3344  abf  3376  disj2  3388  difid  3401  0dif  3404  disjdif  3405  difin0  3406  undif1ss  3407  difdifdirss  3417  rgenm  3435  iftruei  3450  iffalsei  3453  ifbieq2i  3465  ifbieq12i  3467  pweqi  3484  pwid  3495  sneqi  3509  elsn  3513  elpr  3518  elsn2  3529  ralsn  3537  rexsn  3538  eltp  3541  rabrsndc  3561  preq1i  3573  preq2i  3574  prid1  3599  snnz  3612  snm  3613  prnz  3615  prm  3616  tpnz  3618  snsssn  3658  opeq1i  3678  opeq2i  3679  unieqi  3716  unissi  3729  inteqi  3745  intmin2  3767  intab  3770  intsn  3776  iinconstm  3792  iuniin  3793  iinss1  3795  iunxdif2  3831  ssiinf  3832  iinss  3834  iinss2  3835  iinab  3844  iundif2ss  3848  iindif2m  3850  iinin2m  3851  iunxsn  3859  iunxprg  3863  iinpw  3873  sndisj  3895  disjxsn  3897  breqi  3905  breq1i  3906  breq2i  3907  brab1  3945  opabbii  3965  truni  4010  bm1.3ii  4019  a9evsep  4020  ax9vsep  4021  zfnuleu  4022  axnul  4023  ssexi  4036  rabex  4042  elpw2  4052  pwnss  4053  iin0r  4063  intv  4064  pwex  4077  snex  4079  notnotsnex  4081  ord3ex  4084  dtruarb  4085  undifexmid  4087  intid  4116  opnzi  4127  copsexg  4136  opelopabf  4166  epelc  4183  elon  4266  inton  4285  onn0  4292  onm  4293  elsuc  4298  elsuc2  4299  sucid  4309  iunsuc  4312  onordi  4318  ontrci  4319  onelssi  4321  eusvnf  4344  ssonunii  4375  sucex  4385  onssi  4401  onsuci  4402  ordtriexmidlem  4405  ordtriexmidlem2  4406  ordtriexmid  4407  ordtri2orexmid  4408  2ordpr  4409  ontr2exmid  4410  onsucsssucexmid  4412  onsucelsucexmid  4415  regexmidlemm  4417  reg2exmid  4421  onirri  4428  ruALT  4436  onprc  4437  sucon  4438  dtru  4445  0elsucexmid  4450  ordpwsucexmid  4455  ordtri2or2exmid  4456  dcextest  4465  omex  4477  find  4483  omelon  4492  nnoni  4494  limom  4497  nnregexmid  4504  omsinds  4505  xpeq1i  4529  xpeq2i  4530  0nelxp  4537  opthprc  4560  mosubop  4575  releqi  4592  relssi  4600  relin1  4627  relin2  4628  reldif  4629  inopab  4641  difopab  4642  xpiindim  4646  opabbi2dv  4658  ideq  4661  coeq1i  4668  coeq2i  4669  cnveqi  4684  eldm  4706  eldm2  4707  dmeqi  4710  dmv  4725  rneqi  4737  elrnmpti  4762  dmex  4775  rnex  4776  reseq1i  4785  reseq2i  4786  residm  4821  resex  4830  resmpt3  4838  imaeq1i  4848  imaeq2i  4849  elima  4856  imaex  4864  elimasn  4876  args  4878  epini  4880  dfse2  4882  relbrcnv  4889  cotr  4890  issref  4891  cnvsym  4892  asymref  4894  intirr  4895  codir  4897  qfto  4898  ssrnres  4951  cnveq0  4965  cnvsn0  4977  dmsnop  4982  rnsnop  4989  resdm2  4999  dfco2a  5009  cocnvcnv1  5019  coi2  5025  coires1  5026  cnvssrndm  5030  cossxp  5031  cocnvres  5033  relrelss  5035  relcoi2  5039  unidmrn  5041  dfdm2  5043  unixpm  5044  cnvexg  5046  cnvex  5047  cnviinm  5050  iotaval  5069  funeqi  5114  funi  5125  funres  5134  funcnvsn  5138  funcnvcnv  5152  funin  5164  funcnvres  5166  isarep2  5180  fneq1i  5187  fneq2i  5188  fnresdisj  5203  fnresi  5210  mpt0  5220  dmmpti  5222  feq1i  5235  feq2i  5236  fdmi  5250  fun2  5266  fssres  5268  resasplitss  5272  fintm  5278  fconst6  5292  f1ores  5350  foimacnv  5353  resdif  5357  funcocnv2  5360  f1ovi  5374  fveq1i  5390  fveq2i  5392  0fv  5424  fvun1  5455  fvopab3ig  5463  fvmptss2  5464  mptrcl  5471  elfvmptrab1  5483  fndmdif  5493  fneqeql2  5497  f1oresrab  5553  fmptco  5554  fnressn  5574  fressnfv  5575  fmptap  5578  fvsnun1  5585  fvsnun2  5586  fsnunfv  5589  fconst2  5605  mptex  5614  riotabiia  5715  acexmidlema  5733  acexmidlemb  5734  acexmidlemcase  5737  acexmidlem2  5739  acexmidlemv  5740  oveq1i  5752  oveq2i  5753  oveqi  5755  oprabidlem  5770  0neqopab  5784  oprabbii  5794  oprabss  5825  mpompt  5831  funoprab  5839  fnoprab  5842  fovcl  5844  ovigg  5859  elmpocl  5936  resfunexgALT  5976  cofunexg  5977  opabex3d  5987  opabex3  5988  1st0  6010  2nd0  6011  op1st  6012  op2nd  6013  f1stres  6025  f2ndres  6026  fo1stresm  6027  fo2ndresm  6028  1stcof  6029  2ndcof  6030  1stexg  6033  2ndexg  6034  releldm2  6051  reldm  6052  dfoprab3  6057  mpomptsx  6063  mpompts  6064  fnmpoi  6070  dmmpo  6071  mpoexxg  6076  1stconst  6086  2ndconst  6087  dfmpo  6088  algrflem  6094  algrflemg  6095  cnvoprab  6099  f1od2  6100  mpoxopn0yelv  6104  mpoxopoveq  6105  tposssxp  6114  brtpos2  6116  reldmtpos  6118  dftpos2  6126  dftpos4  6128  tpostpos  6129  tpostpos2  6130  tposfo  6136  tposf  6137  tposeqi  6142  tposex  6143  tposoprab  6145  issmo  6153  smores  6157  smores2  6159  iordsmo  6162  smo0  6163  tfrlem8  6183  tfrexlem  6199  tfr1onlem3  6203  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlemres  6214  tfri1dALT  6216  tfri2  6231  rdgisuc1  6249  rdg0  6252  frecfun  6260  frec0g  6262  freccllem  6267  frecfcllem  6269  frecsuclem  6271  frecrdg  6273  2on0  6291  xp01disj  6298  2oconcl  6304  fnoa  6311  oaexg  6312  fnom  6314  omexg  6315  fnoei  6316  oeiexg  6317  oei0  6323  oacl  6324  oasuc  6328  o1p1e2  6332  omsuc  6336  nna0r  6342  nnm0r  6343  1onn  6384  2onn  6385  3onn  6386  4onn  6387  eqerlem  6428  elqs  6448  qsex  6454  ecqs  6459  iinerm  6469  th3qlem1  6499  th3q  6502  mapsn  6552  mapsnf1o3  6559  ixpiinm  6586  ixpssmap  6594  brdom  6612  f1dom  6622  enref  6627  dom2  6637  idssen  6639  ssdomg  6640  ensymi  6644  ensn1  6658  fiprc  6677  1domsn  6681  xpcomf1o  6687  xpcomco  6688  dom0  6700  0dom  6701  xpmapenlem  6711  phplem2  6715  php5  6720  snnen2og  6721  1nen2  6723  php5dom  6725  ssfilem  6737  ssfiexmid  6738  domfiexmid  6740  0fin  6746  diffitest  6749  findcard  6750  findcard2  6751  findcard2s  6752  isinfinf  6759  ac6sfi  6760  inffiexmid  6768  unfiexmid  6774  xpfi  6786  fisseneq  6788  ssfirab  6790  en1eqsn  6804  snexxph  6806  sbthlem2  6814  sbthlemi3  6815  sbthlemi6  6818  sbthlem7  6819  fi0  6831  supeq1i  6843  infeq1i  6868  djuexb  6897  djuf1olemr  6907  inresflem  6913  djuinr  6916  updjudhcoinlf  6933  updjudhcoinrg  6934  casefun  6938  caserel  6940  caseinj  6942  caseinl  6944  caseinr  6945  omp1eomlem  6947  endjusym  6949  difinfsn  6953  difinfinf  6954  djuinj  6959  0ct  6960  ctmlemr  6961  ctssdclemn0  6963  ctssdccl  6964  omct  6970  ctfoex  6971  finomni  6980  exmidomni  6982  fodjuomni  6989  nnnninf  6991  ctssexmid  6992  fodjumkv  7002  card0  7012  exmidonfinlem  7017  dju1p1e2  7021  exmidfodomrlemim  7025  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  0npi  7089  dmaddpi  7101  dmmulpi  7102  1lt2pi  7116  0nnq  7140  1nq  7142  dmaddpq  7155  dmmulpq  7156  rec1nq  7171  1lt2nq  7182  halfnqq  7186  prarloclemarch2  7195  enq0enq  7207  nqnq0pi  7214  nnnq0lem1  7222  addnnnq0  7225  mulnnnq0  7226  nq0m0r  7232  addpinq1  7240  prarloclem5  7276  prarloclemcalc  7278  1pr  7330  1idprl  7366  1idpru  7367  ltexprlemm  7376  recexprlem1ssl  7409  recexprlem1ssu  7410  suplocexprlemell  7489  suplocexprlem2b  7490  suplocexprlemmu  7494  suplocexprlemdisj  7496  suplocexprlemloc  7497  suplocexprlemub  7499  suplocexprlemlub  7500  prsrlem1  7518  addsrpr  7521  mulsrpr  7522  gt0srpr  7524  0nsr  7525  0r  7526  1sr  7527  m1r  7528  m1m1sr  7537  caucvgsr  7578  suplocsrlempr  7583  addresr  7613  mulresr  7614  pitonnlem1  7621  peano1nnnn  7628  axi2m1  7651  axcnre  7657  peano5nnnn  7668  axcaucvg  7676  mulid1i  7736  mulid2i  7737  pnfnre  7775  mnfnre  7776  pnfnemnf  7788  mnfxr  7790  rexri  7791  ltnri  7824  ltleii  7834  00id  7871  addid1i  7872  addid2i  7873  0cnALT  7920  negeqi  7924  negicn  7931  neg0  7976  renegcli  7992  negcli  7998  negidi  7999  negnegi  8000  subidi  8001  subid1i  8002  negne0bi  8003  negrebi  8004  mul02i  8120  mul01i  8121  mulm1i  8133  leidi  8215  gt0ne0ii  8217  inelr  8313  msqge0i  8346  gt0ap0ii  8357  1div1e1  8431  div1i  8467  eqnegi  8468  recclapi  8469  recidapi  8470  divmulapi  8493  rerecclapi  8504  redivclapi  8506  recgt0  8572  ltp1i  8627  divgt0ii  8641  ltmul1ii  8650  ltdiv1ii  8651  sup3exmid  8679  peano5nni  8687  nnrei  8693  1nn  8695  nngt0i  8714  neg1ap0  8793  2timesi  8808  times2i  8809  2nn  8839  3nn  8840  4nn  8841  5nn  8842  6nn  8843  7nn  8844  8nn  8845  9nn  8846  2muline0  8903  rehalfcli  8926  nn0ssre  8939  nnnn0i  8943  dfn2  8948  0nn0  8950  nn0ge0i  8962  zrei  9018  neg1z  9044  nn0negzi  9047  dfz2  9081  nneoi  9113  peano5uzi  9118  dfuzi  9119  nn0ind-raph  9126  deceq1i  9146  deceq2i  9147  10nn  9155  numltc  9165  eluzel2  9287  eluz1i  9289  nn0uz  9316  nnuz  9317  infrenegsupex  9345  lbzbi  9364  divfnzn  9369  qdivcl  9391  irrmul  9395  cnref1o  9396  0ltpnf  9523  mnflt0  9525  0lepnf  9531  xrltnsym  9534  xrlttri3  9538  nltpnft  9552  ngtmnft  9555  xrrebnd  9557  xnegmnf  9567  xneg0  9569  xltnegi  9573  xaddmnf1  9586  xaddmnf2  9587  mnfaddpnf  9589  xaddid1  9600  xnn0lenn0nn0  9603  xnn0xadd0  9605  xposdif  9620  ixxex  9637  iooval2  9653  unirnioo  9711  ioorebasg  9713  elrege0  9714  fzval2  9748  fzen  9778  fzprval  9817  fztpval  9818  uzdisj  9828  ige2m1fz  9845  fz01or  9846  fz1ssfz0  9852  fz0tp  9856  nn0disj  9870  1fv  9871  4fvwrd4  9872  fzo0ss1  9906  fzo01  9948  fzo12sn  9949  fzo0to2pr  9950  fzo0to3tp  9951  fzo0to42pr  9952  qbtwnxr  9990  flval  10000  modqfrac  10065  modqmulnn  10070  q2txmodxeq0  10112  frecuzrdgdom  10146  frecuzrdgfun  10148  frecuzrdgsuct  10152  frechashgf1o  10156  nnct  10163  fxnn0nninf  10166  0tonninf  10167  1tonninf  10168  iseqvalcbv  10185  ser0f  10243  0exp0e1  10253  qexpcl  10264  qexpclz  10269  m1expcl2  10270  1exp  10277  sqvali  10327  sqcli  10328  sqeq0i  10329  resqcli  10332  sq1  10341  neg1sqe1  10342  iexpcyc  10352  facnn  10428  fac0  10429  fac1  10430  fac2  10432  fac3  10433  fac4  10434  bcval  10450  bcm1k  10461  bcpasc  10467  bccl  10468  4bc3eq4  10474  4bc2eq6  10475  hashinfom  10479  hashennn  10481  hashfz1  10484  fihasheq0  10495  hash0  10498  hashsng  10499  fihashen1  10500  omgadd  10503  hashp1i  10511  hashxp  10527  fimaxq  10528  zfz1iso  10539  shftidt2  10559  cjexp  10620  re0  10622  im0  10623  re1  10624  im1  10625  cj0  10628  cji  10629  recli  10638  imcli  10639  cjcli  10640  replimi  10641  cjcji  10642  reim0bi  10643  rerebi  10644  cjrebi  10645  recji  10646  imcji  10647  cjmulrcli  10648  cjmulvali  10649  cjmulge0i  10650  renegi  10651  imnegi  10652  cjnegi  10653  addcji  10654  uzin2  10714  rexanuz  10715  rexfiuz  10716  sqrtrval  10727  sqrt0  10731  resqrexlemcalc3  10743  resqrexlemcvg  10746  resqrex  10753  abs0  10785  absi  10786  qabsor  10802  absimle  10811  recan  10836  caubnd2  10844  leabsi  10855  absrei  10856  sqrtpclii  10857  sqrtgt0ii  10858  absvalsqi  10867  absvalsq2i  10868  abscli  10869  absge0i  10870  absval2i  10871  abs00i  10872  absgt0api  10873  absnegi  10874  abscji  10875  releabsi  10876  infxrnegsupex  10987  xrbdtri  11000  cbvsum  11084  sumeq1i  11087  sum0  11112  isumz  11113  fisumss  11116  fsumsersdc  11119  fsumadd  11130  isumclim  11145  isumclim3  11147  fsumcnv  11161  modfsummodlem1  11180  fsumrelem  11195  binomlem  11207  binom  11208  arisum2  11223  expcnv  11228  0.999...  11245  ef0lem  11280  esum  11282  ere  11290  ege2le3  11291  ef0  11292  eff2  11300  efsep  11311  reeff1  11321  sin0  11350  cos0  11351  ef01bndlem  11377  cos2bnd  11381  sincos1sgn  11385  sincos2sgn  11386  sin4lt0  11387  eirr  11397  0dvds  11425  dvds1  11463  z0even  11520  n2dvdsm1  11522  z2even  11523  n2dvds3  11524  ndvdssub  11539  ndvdsi  11542  flodddiv4  11543  gcddvds  11564  gcd1  11587  6gcd4e2  11595  bezoutlembi  11605  dfgcd3  11610  dfgcd2  11614  lcmval  11656  lcmcllem  11660  lcmledvds  11663  3lcm2e6woprm  11679  qredeu  11690  isprm2lem  11709  isprm3  11711  prm2orodd  11719  pw2dvds  11755  phicl2  11801  phi1  11806  dfphi2  11807  phiprmpw  11809  ennnfonelemp1  11830  ennnfonelem1  11831  ennnfonelemkh  11836  ennnfonelemex  11838  ennnfonelemnn0  11846  ennnfonelemr  11847  exmidunben  11850  ctinfomlemom  11851  ctinfom  11852  ctinf  11854  qnnen  11855  structcnvcnv  11886  structfun  11888  structfn  11889  ndxarg  11893  ndxid  11894  setsresg  11908  setsslnid  11921  strleun  11959  strle1g  11960  istopon  12091  topontopi  12094  toponunii  12095  toponrestid  12099  istps  12110  topontopn  12115  eltpsi  12119  eltg4i  12135  eltg3  12137  tg1  12139  tg2  12140  tgclb  12145  topnex  12166  sn0topon  12168  distps  12171  cldrcl  12182  sn0cld  12217  restco  12254  lmrcl  12271  ssidcn  12290  cnconst2  12313  cnptopresti  12318  cnptoprest  12319  txuni2  12336  txbas  12338  eltx  12339  txcnp  12351  upxp  12352  txcnmpt  12353  uptx  12354  txcn  12355  txrest  12356  txlm  12359  cnmptid  12361  cnmpt1st  12368  cnmpt2nd  12369  hmeofn  12382  psmetge0  12411  ismeti  12426  xmetunirn  12438  xmetge0  12445  unirnblps  12502  unirnbl  12503  mopnex  12585  qtopbasss  12601  retop  12604  uniretop  12605  iooretopg  12608  cnxmet  12611  cntoptopon  12612  cnbl0  12614  rexmet  12621  blssioo  12625  tgioo  12626  tgqioo  12627  cnopnap  12674  limcresi  12715  dvfvalap  12730  dvidlemap  12740  dvcnp2cntop  12743  dvcoapbr  12751  dvexp2  12756  dvrecap  12757  dveflem  12766  dvef  12767  sin0pilem1  12773  sin0pilem2  12774  pilem3  12775  pigt2lt4  12776  pire  12778  sinhalfpilem  12783  pidiv2halves  12787  cosneghalfpi  12790  cospi  12792  efipi  12793  sin2pi  12795  cos2pi  12796  ef2pi  12797  cosq14gt0  12824  coseq00topi  12827  coseq0negpitopi  12828  ex-fl  12833  ex-ceil  12834  ex-exp  12835  ex-fac  12836  ex-gcd  12839  bj-dcdc  12861  bj-stdc  12862  bj-dcst  12863  bj-stst  12864  bj-el2oss1o  12877  elabf2  12885  bd0  12918  bdeli  12940  bdcriota  12977  bdbm1.3ii  12985  bdinex1  12993  bdssexi  12997  bj-inex  13001  bj-snex  13007  bj-sucex  13017  bj-d0clsepcl  13019  bj-omind  13028  bj-om  13031  bj-2inf  13032  bj-peano2  13033  bdpeano5  13037  bj-omssonALT  13057  bj-inf2vnlem1  13064  bj-omex2  13071  bj-nn0sucALT  13072  subctctexmid  13092  nninfall  13100  nninfsellemqall  13107  nninfsellemeqinf  13108  nninfomnilem  13110  nninfomni  13111  exmidsbthrlem  13113  sbthom  13117  isomninnlem  13121  isomninn  13122  cvgcmp2nlemabs  13123  trilpolemisumle  13127  trilpolemeq1  13129  trilpo  13132
  Copyright terms: Public domain W3C validator