ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-mp GIF 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 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  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  948  simp2i  949  simp3i  950  3mix1i  1111  3mix2i  1112  3mix3i  1113  3jaoi  1235  trud  1294  dfnot  1303  mptnan  1355  mtpor  1357  mtpxor  1358  mpg  1381  19.23h  1428  hbequid  1447  axi12  1448  nfri  1453  spi  1470  19.21  1516  eximii  1534  19.35i  1557  nfn  1589  19.37aiv  1606  19.23  1609  exan  1624  equid  1630  hbae  1648  equvini  1683  equveli  1684  sbid  1699  sbieh  1715  exdistrfor  1723  dveeq2or  1739  ax11v  1750  ax11ev  1751  equs5or  1753  sb4or  1756  sb4bor  1758  nfsb2or  1760  sbequilem  1761  sbequi  1762  speiv  1785  nfsbxy  1861  nfsbxyt  1862  sbco  1885  sbcocom  1887  sbcomxyyz  1889  elsb3  1895  elsb4  1896  sbal1yz  1920  dvelimALT  1929  dvelimfv  1930  dvelimor  1937  eumoi  1976  moani  2013  eqeq1i  2090  eqeq2i  2093  eleq1i  2148  eleq2i  2149  nfcrii  2216  neeq1i  2264  neeq2i  2265  necon3i  2297  rspec  2421  rgen2a  2423  mprg  2426  r19.21  2443  r19.23  2474  raleqi  2559  rexeqi  2560  rabeqif  2603  elexi  2622  ceqsal  2639  vtocl3  2666  vtoclef  2682  vtocle  2683  spcv  2702  spcev  2703  clel3  2740  elabf  2747  elab2  2751  elab3  2755  euxfrdc  2789  reueq  2800  rmoimi2  2804  sbsbc  2830  sbc8g  2833  sbc6  2851  sbcie  2859  sbcrex  2904  csbvarg  2944  csbief  2958  csbie2  2962  sbnfc2  2973  sseli  3006  sselii  3007  sseq1i  3034  sseq2i  3035  difeq1i  3098  difeq2i  3099  uneq1i  3134  uneq2i  3135  ineq1i  3181  ineq2i  3182  ssinss1  3212  difdif2ss  3239  vn0  3276  vn0m  3277  abf  3308  disj2  3320  difid  3333  0dif  3336  disjdif  3337  difin0  3338  undif1ss  3339  difdifdirss  3348  rgenm  3365  iftruei  3379  iffalsei  3382  ifbieq2i  3394  ifbieq12i  3396  pweqi  3410  pwid  3420  sneqi  3434  elsn  3438  elpr  3443  elsn2  3452  ralsn  3460  rexsn  3461  eltp  3464  rabrsndc  3484  preq1i  3496  preq2i  3497  prid1  3522  snnz  3533  snm  3534  prnz  3536  prm  3537  tpnz  3539  snsssn  3579  opeq1i  3599  opeq2i  3600  unieqi  3637  unissi  3650  inteqi  3666  intmin2  3688  intab  3691  intsn  3697  iinconstm  3713  iuniin  3714  iinss1  3716  iunxdif2  3752  ssiinf  3753  iinss  3755  iinss2  3756  iinab  3765  iundif2ss  3769  iindif2m  3771  iinin2m  3772  iunxsn  3780  iinpw  3789  sndisj  3807  disjxsn  3809  breqi  3817  breq1i  3818  breq2i  3819  brab1  3856  opabbii  3871  truni  3915  bm1.3ii  3925  a9evsep  3926  ax9vsep  3927  zfnuleu  3928  axnul  3929  ssexi  3942  rabex  3948  elpw2  3958  pwnss  3959  iin0r  3969  intv  3970  snex  3983  notnotsnex  3985  ord3ex  3988  dtruarb  3989  undifexmid  3991  intid  4014  opnzi  4025  copsexg  4034  opelopabf  4064  epelc  4081  elon  4164  inton  4183  onn0  4190  onm  4191  elsuc  4196  elsuc2  4197  sucid  4207  iunsuc  4210  onordi  4216  ontrci  4217  onelssi  4219  eusvnf  4238  ssonunii  4268  sucex  4278  onssi  4294  onsuci  4295  ordtriexmidlem  4298  ordtriexmidlem2  4299  ordtriexmid  4300  ordtri2orexmid  4301  2ordpr  4302  ontr2exmid  4303  onsucsssucexmid  4305  onsucelsucexmid  4308  regexmidlemm  4310  reg2exmid  4314  onirri  4321  ruALT  4329  onprc  4330  sucon  4331  dtru  4338  0elsucexmid  4343  ordpwsucexmid  4348  ordtri2or2exmid  4349  dcextest  4358  omex  4370  find  4376  omelon  4385  nnoni  4387  limom  4390  nnregexmid  4396  omsinds  4397  xpeq1i  4420  xpeq2i  4421  0nelxp  4427  opthprc  4446  mosubop  4461  releqi  4478  relssi  4486  relin1  4512  relin2  4513  reldif  4514  inopab  4525  difopab  4526  xpiindim  4530  opabbi2dv  4542  ideq  4545  coeq1i  4552  coeq2i  4553  cnveqi  4568  eldm  4590  eldm2  4591  dmeqi  4594  dmv  4609  rneqi  4620  elrnmpti  4645  dmex  4656  rnex  4657  reseq1i  4666  reseq2i  4667  residm  4700  resex  4709  resmpt3  4717  imaeq1i  4725  imaeq2i  4726  elima  4733  imaex  4741  elimasn  4753  args  4755  epini  4757  dfse2  4759  relbrcnv  4766  cotr  4767  issref  4768  cnvsym  4769  asymref  4771  intirr  4772  codir  4774  qfto  4775  ssrnres  4826  cnveq0  4840  cnvsn0  4852  dmsnop  4857  rnsnop  4864  resdm2  4874  dfco2a  4884  cocnvcnv1  4894  coi2  4900  coires1  4901  cnvssrndm  4905  cossxp  4906  cocnvres  4908  relrelss  4910  relcoi2  4914  unidmrn  4916  dfdm2  4918  unixpm  4919  cnvexg  4921  cnvex  4922  cnviinm  4925  iotaval  4944  funeqi  4988  funi  4998  funres  5007  funcnvsn  5011  funcnvcnv  5025  funin  5037  funcnvres  5039  isarep2  5053  fneq1i  5060  fneq2i  5061  fnresdisj  5076  fnresi  5083  mpt0  5093  dmmpti  5095  feq1i  5106  feq2i  5107  fdmi  5119  fun2  5132  fssres  5134  resasplitss  5137  fintm  5143  fconst6  5157  f1ores  5215  foimacnv  5218  resdif  5222  funcocnv2  5225  f1ovi  5239  fveq1i  5253  fveq2i  5255  0fv  5283  fvun1  5314  fvopab3ig  5322  fvmptss2  5323  fndmdif  5348  fneqeql2  5352  f1oresrab  5404  fmptco  5405  fnressn  5424  fressnfv  5425  fmptap  5428  fvsnun1  5435  fvsnun2  5436  fsnunfv  5438  fconst2  5453  mptex  5462  riotabiia  5563  acexmidlema  5581  acexmidlemb  5582  acexmidlemcase  5585  acexmidlem2  5587  acexmidlemv  5588  oveq1i  5600  oveq2i  5601  oveqi  5603  oprabidlem  5614  0neqopab  5628  oprabbii  5638  oprabss  5668  mpt2mpt  5674  funoprab  5679  fnoprab  5682  fovcl  5684  ovigg  5699  elmpt2cl  5776  resfunexgALT  5815  cofunexg  5816  opabex3d  5826  opabex3  5827  1st0  5849  2nd0  5850  op1st  5851  op2nd  5852  f1stres  5864  f2ndres  5865  fo1stresm  5866  fo2ndresm  5867  1stcof  5868  2ndcof  5869  1stexg  5872  2ndexg  5873  releldm2  5889  reldm  5890  dfoprab3  5895  mpt2mptsx  5901  mpt2mpts  5902  fnmpt2i  5908  dmmpt2  5909  mpt2exxg  5911  1stconst  5920  2ndconst  5921  dfmpt2  5922  algrflem  5928  algrflemg  5929  cnvoprab  5933  f1od2  5934  mpt2xopn0yelv  5935  mpt2xopoveq  5936  tposssxp  5945  brtpos2  5947  reldmtpos  5949  dftpos2  5957  dftpos4  5959  tpostpos  5960  tpostpos2  5961  tposfo  5967  tposf  5968  tposeqi  5973  tposex  5974  tposoprab  5976  issmo  5984  smores  5988  smores2  5990  iordsmo  5993  smo0  5994  tfrlem8  6014  tfrexlem  6030  tfr1onlem3  6034  tfr1onlemsucaccv  6037  tfr1onlembxssdm  6039  tfr1onlemres  6045  tfri1dALT  6047  tfri2  6062  rdgisuc1  6080  rdg0  6083  frecfun  6091  frec0g  6093  freccllem  6098  frecfcllem  6100  frecsuclem  6102  frecrdg  6104  2on0  6122  xp01disj  6129  2oconcl  6134  fnoa  6139  oaexg  6140  fnom  6142  omexg  6143  fnoei  6144  oeiexg  6145  oei0  6151  oacl  6152  oasuc  6156  o1p1e2  6160  omsuc  6164  nna0r  6170  nnm0r  6171  1onn  6208  2onn  6209  3onn  6210  4onn  6211  eqerlem  6252  elqs  6272  qsex  6278  ecqs  6283  iinerm  6293  th3qlem1  6323  th3q  6326  mapsn  6376  mapsnf1o3  6383  brdom  6396  f1dom  6406  enref  6411  dom2  6421  idssen  6423  ssdomg  6424  ensymi  6428  ensn1  6442  fiprc  6461  1domsn  6464  xpcomf1o  6470  xpcomco  6471  dom0  6483  0dom  6484  xpmapenlem  6494  phplem2  6498  php5  6503  snnen2og  6504  1nen2  6506  php5dom  6508  ssfilem  6520  ssfiexmid  6521  domfiexmid  6523  0fin  6529  diffitest  6532  findcard  6533  findcard2  6534  findcard2s  6535  isinfinf  6542  ac6sfi  6543  inffiexmid  6548  unfiexmid  6554  xpfi  6564  fisseneq  6566  ssfirab  6567  en1eqsn  6580  snexxph  6582  supeq1i  6589  infeq1i  6614  djuf1olemr  6652  inresflem  6658  djuinr  6661  djuun  6666  updjudhcoinlf  6677  updjudhcoinrg  6678  casefun  6682  caserel  6684  caseinj  6686  djuinj  6692  finomni  6700  exmidomniim  6701  exmidomni  6702  fodjuomni  6708  card0  6718  dju1p1e2  6725  exmidfodomrlemim  6729  exmidfodomrlemr  6730  exmidfodomrlemrALT  6731  0npi  6774  dmaddpi  6786  dmmulpi  6787  1lt2pi  6801  0nnq  6825  1nq  6827  dmaddpq  6840  dmmulpq  6841  rec1nq  6856  1lt2nq  6867  halfnqq  6871  prarloclemarch2  6880  enq0enq  6892  nqnq0pi  6899  nnnq0lem1  6907  addnnnq0  6910  mulnnnq0  6911  nq0m0r  6917  addpinq1  6925  prarloclem5  6961  prarloclemcalc  6963  1pr  7015  1idprl  7051  1idpru  7052  ltexprlemm  7061  recexprlem1ssl  7094  recexprlem1ssu  7095  prsrlem1  7190  addsrpr  7193  mulsrpr  7194  gt0srpr  7196  0nsr  7197  0r  7198  1sr  7199  m1r  7200  m1m1sr  7209  caucvgsr  7249  addresr  7276  mulresr  7277  pitonnlem1  7284  peano1nnnn  7291  axi2m1  7312  axcnre  7318  peano5nnnn  7329  axcaucvg  7337  mulid1i  7392  mulid2i  7393  pnfnre  7431  mnfnre  7432  pnfnemnf  7444  mnfxr  7446  rexri  7447  ltnri  7479  ltleii  7489  00id  7525  addid1i  7526  addid2i  7527  0cnALT  7574  negeqi  7578  negicn  7585  neg0  7630  renegcli  7646  negcli  7652  negidi  7653  negnegi  7654  subidi  7655  subid1i  7656  negne0bi  7657  negrebi  7658  mul02i  7770  mul01i  7771  mulm1i  7783  leidi  7862  gt0ne0ii  7864  inelr  7960  msqge0i  7993  gt0ap0ii  8003  1div1e1  8068  div1i  8104  eqnegi  8105  recclapi  8106  recidapi  8107  divmulapi  8130  rerecclapi  8141  redivclapi  8143  recgt0  8204  ltp1i  8259  divgt0ii  8273  ltmul1ii  8282  ltdiv1ii  8283  peano5nni  8318  nnrei  8324  1nn  8326  nngt0i  8345  neg1ap0  8424  2timesi  8438  times2i  8439  2nn  8469  3nn  8470  4nn  8471  5nn  8472  6nn  8473  7nn  8474  8nn  8475  9nn  8476  2muline0  8532  rehalfcli  8555  nn0ssre  8568  nnnn0i  8572  dfn2  8577  0nn0  8579  nn0ge0i  8591  nnnninf  8644  zrei  8651  neg1z  8677  nn0negzi  8680  dfz2  8714  nneoi  8745  peano5uzi  8750  dfuzi  8751  nn0ind-raph  8758  deceq1i  8777  deceq2i  8778  10nn  8786  numltc  8796  eluzel2  8918  eluz1i  8920  nn0uz  8947  nnuz  8948  infrenegsupex  8976  lbzbi  8995  divfnzn  9000  qdivcl  9022  irrmul  9026  cnref1o  9027  0ltpnf  9146  mnflt0  9148  0lepnf  9154  xrltnsym  9157  xrlttri3  9161  nltpnft  9173  ngtmnft  9174  xrrebnd  9175  xnegmnf  9185  xneg0  9187  xltnegi  9191  ixxex  9211  iooval2  9227  unirnioo  9285  ioorebasg  9287  elrege0  9288  fzval2  9321  fzen  9351  fzprval  9388  fztpval  9389  uzdisj  9399  ige2m1fz  9416  fz01or  9417  fz0tp  9425  nn0disj  9438  1fv  9439  4fvwrd4  9440  fzo0ss1  9473  fzo01  9515  fzo12sn  9516  fzo0to2pr  9517  fzo0to3tp  9518  fzo0to42pr  9519  qbtwnxr  9557  flval  9567  modqfrac  9632  modqmulnn  9637  q2txmodxeq0  9679  frecuzrdgdom  9713  frecuzrdgfun  9715  frecuzrdgsuct  9719  frechashgf1o  9723  nnct  9730  fxnn0nninf  9732  0tonninf  9733  1tonninf  9734  iseqvalcbv  9749  iser0f  9787  0exp0e1  9796  qexpcl  9807  qexpclz  9812  m1expcl2  9813  1exp  9820  sqvali  9870  sqcli  9871  sqeq0i  9872  resqcli  9875  sq1  9884  neg1sqe1  9885  iexpcyc  9894  facnn  9969  fac0  9970  fac1  9971  fac2  9973  fac3  9974  fac4  9975  bcval  9991  bcm1k  10002  ibcval5  10005  bcpasc  10008  bccl  10009  4bc3eq4  10015  4bc2eq6  10016  hashinfom  10020  hashennn  10022  hashfz1  10025  fihasheq0  10036  hash0  10039  hashsng  10040  fihashen1  10041  omgadd  10044  hashp1i  10052  hashxp  10068  shftidt2  10093  cjexp  10153  re0  10155  im0  10156  re1  10157  im1  10158  cj0  10161  cji  10162  recli  10171  imcli  10172  cjcli  10173  replimi  10174  cjcji  10175  reim0bi  10176  rerebi  10177  cjrebi  10178  recji  10179  imcji  10180  cjmulrcli  10181  cjmulvali  10182  cjmulge0i  10183  renegi  10184  imnegi  10185  cjnegi  10186  addcji  10187  uzin2  10246  rexanuz  10247  rexfiuz  10248  sqrtrval  10259  sqrt0  10263  resqrexlemcalc3  10275  resqrexlemcvg  10278  resqrex  10285  abs0  10317  absi  10318  qabsor  10334  absimle  10343  recan  10368  caubnd2  10376  leabsi  10387  absrei  10388  sqrtpclii  10389  sqrtgt0ii  10390  absvalsqi  10399  absvalsq2i  10400  abscli  10401  absge0i  10402  absval2i  10403  abs00i  10404  absgt0api  10405  absnegi  10406  abscji  10407  releabsi  10408  0dvds  10595  dvds1  10633  z0even  10690  n2dvdsm1  10692  z2even  10693  n2dvds3  10694  ndvdssub  10709  ndvdsi  10712  flodddiv4  10713  gcddvds  10734  gcd1  10757  6gcd4e2  10763  bezoutlembi  10773  dfgcd3  10778  dfgcd2  10782  eucialg  10820  lcmval  10824  lcmcllem  10828  lcmledvds  10831  3lcm2e6woprm  10847  qredeu  10858  isprm2lem  10877  isprm3  10879  prm2orodd  10887  pw2dvds  10923  phicl2  10969  phi1  10974  dfphi2  10975  phiprmpw  10977  ex-fl  10995  ex-ceil  10996  ex-fac  10997  ex-gcd  11000  elabf2  11024  bd0  11057  bdeli  11079  bdcriota  11116  bdbm1.3ii  11124  bdinex1  11132  bdssexi  11136  bj-inex  11140  bj-snex  11146  bj-sucex  11156  bj-notbii  11159  bj-d0clsepcl  11162  bj-omind  11171  bj-om  11174  bj-2inf  11175  bj-peano2  11176  bdpeano5  11180  bj-omssonALT  11200  bj-inf2vnlem1  11207  bj-omex2  11214  bj-nn0sucALT  11215
  Copyright terms: Public domain W3C validator