New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax-mp Unicode version

Axiom ax-mp 8
 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 mood that by affirming affirms" [Sanford] p. 39. This rule is similar to the rule of modus tollens mto 167. 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
 Colors of variables: wff setvar class This axiom is referenced by:  mp2b  9  a1i  10  mp1i  11  a2i  12  mpd  14  mp2  17  idALT  20  notnotri  106  notnoti  115  pm2.24ii  124  mt4  129  pm2.61i  156  bi1  178  bi3  179  dfbi1  184  dfbi1gb  185  biimpi  186  bicomi  193  mpbi  199  mpbir  200  imbi1i  315  a1bi  327  tbt  333  nbn  336  biorfi  396  simpli  444  simpri  448  biantru  491  biantrur  492  mp2an  653  simp1i  964  simp2i  965  simp3i  966  3mix1i  1127  3mix2i  1128  3mix3i  1129  3jaoi  1245  nanbi1i  1298  nanbi2i  1299  trud  1323  merlem1  1407  merlem2  1408  merlem3  1409  merlem4  1410  merlem5  1411  merlem6  1412  merlem7  1413  merlem8  1414  merlem9  1415  merlem10  1416  merlem11  1417  merlem12  1418  merlem13  1419  luk-1  1420  luk-2  1421  luk-3  1422  luklem1  1423  luklem2  1424  luklem4  1426  luklem6  1428  luklem7  1429  luklem8  1430  ax2  1432  nic-mp  1436  nic-mpALT  1437  tbwsyl  1469  tbwlem2  1471  tbwlem3  1472  tbwlem4  1473  tbwlem5  1474  re1luk2  1476  re1luk3  1477  merco1lem1  1479  retbwax4  1480  retbwax2  1481  merco1lem2  1482  merco1lem3  1483  merco1lem4  1484  merco1lem5  1485  merco1lem6  1486  merco1lem7  1487  retbwax3  1488  merco1lem8  1489  merco1lem9  1490  merco1lem10  1491  merco1lem11  1492  merco1lem12  1493  merco1lem13  1494  merco1lem14  1495  merco1lem15  1496  merco1lem16  1497  merco1lem17  1498  merco1lem18  1499  retbwax1  1500  mercolem1  1502  mercolem2  1503  mercolem3  1504  mercolem4  1505  mercolem5  1506  mercolem6  1507  mercolem7  1508  mercolem8  1509  re1tbw1  1510  re1tbw2  1511  re1tbw3  1512  re1tbw4  1513  anmp  1516  mpto1  1533  mtp-or  1538  mtp-orOLD  1539  mpg  1548  exiftru  1657  spimeh  1667  spimw  1668  19.2OLD  1700  sp  1747  spi  1753  nfri  1762  19.9h  1780  19.9OLD  1784  19.21  1796  19.23  1801  spimehOLD  1821  cbv3hv  1850  exan  1882  sbid  1922  equvini  1987  speiv  2000  sbf  2026  sbco  2083  sbidm  2085  ax11vALT  2097  ax10-16  2190  eumoi  2245  moani  2256  darii  2303  barbari  2305  festino  2309  baroco  2310  cesaro  2311  camestros  2312  datisi  2313  disamis  2314  felapton  2317  darapti  2318  dimatis  2320  fresison  2321  calemos  2322  fesapo  2323  bamalip  2324  eqeq1i  2360  eqeq2i  2363  eleq1i  2416  eleq2i  2417  nfcrii  2482  neeq1i  2526  neeq2i  2527  necon3i  2555  rspec  2678  mprg  2683  r19.21  2700  r19.23  2729  raleqi  2811  rexeqi  2812  elexi  2868  ceqsal  2884  vtoclf  2908  vtoclef  2927  vtocle  2928  spcv  2945  spcev  2946  clel3  2977  elabf  2984  elab2  2988  elab3  2992  euxfr  3022  reueq  3033  rmoimi2  3037  sbsbc  3050  sbc8g  3053  sbc6  3072  sbcie  3080  csbvarg  3163  csbief  3177  csbie2  3181  sbnfc2  3196  elnin  3224  elcompl  3225  nineq1i  3237  nineq2i  3238  compleqi  3244  symdifeq1i  3251  symdifeq2i  3252  sseli  3269  sselii  3270  sseq1i  3295  sseq2i  3296  psseq1i  3358  psseq2i  3359  difeq1i  3381  difeq2i  3382  uneq1i  3414  uneq2i  3415  ineq1i  3453  ineq2i  3454  ssinss1  3483  necompl  3544  vn0  3557  abf  3584  disj2  3598  0dif  3621  ifbieq2i  3681  ifbieq12i  3683  pweqi  3726  pwid  3735  sneqi  3745  elpr  3751  elsnc  3756  elsnc2  3762  ralsn  3767  rexsn  3768  eltp  3771  r19.12sn  3789  preq1i  3802  preq2i  3803  prid1  3827  snnz  3834  prnz  3835  tpnz  3837  sneqb  3876  unieqi  3901  unissi  3914  unidif  3923  inteqi  3930  intmin2  3953  intab  3956  intsn  3962  iinconst  3978  iuniin  3979  iinss1  3981  iunxdif2  4014  ssiinf  4015  iinss  4017  iinss2  4018  iinab  4027  iinun2  4032  iundif2  4033  iindif2  4035  iinin2  4036  iinxprg  4043  iunxsn  4045  iinuni  4049  iinpw  4054  opkeq1i  4062  opkeq2i  4063  complex  4104  snelpw  4115  snel1c  4140  eluni1  4173  xpkeq1i  4201  xpkeq2i  4202  opkabssvvk  4208  cnvkeqi  4216  ins2keqi  4220  ins3keqi  4221  imakeq1i  4226  imakeq2i  4227  cokeq1i  4232  cokeq2i  4233  p6eqi  4239  sikeqi  4242  elimak  4259  elimakv  4260  elp6  4263  sikss1c1c  4267  ins2kss  4279  ins3kss  4280  cnvkexg  4286  cnvkex  4287  p6exg  4290  dfuni12  4291  uni1ex  4293  ssetkex  4294  sikexg  4296  sikex  4297  dfimak2  4298  pw1ex  4303  ins2kexg  4305  ins3kexg  4306  ins2kex  4307  ins3kex  4308  imagekex  4312  uniex  4317  intex  4320  abexv  4324  pwex  4329  iotaval  4350  iota4an  4358  addceq1i  4386  addceq2i  4387  0nelsuc  4400  1cnnc  4408  nndisjeq  4429  leltfintr  4458  tfinnul  4491  tfin0c  4497  tfin1c  4499  0ceven  4505  tncveqnc1fin  4544  vfintle  4546  vfin1cltv  4547  vfinspsslem1  4550  nulnnn  4556  phiex  4572  opeq1i  4581  opeq2i  4582  proj1ex  4593  proj2ex  4594  mosubop  4613  phialllem2  4617  phiall  4618  opabbii  4626  breqi  4645  breq1i  4646  breq2i  4647  ssbri  4681  brab1  4684  opelopabf  4711  siex  4753  xpeq1i  4804  xpeq2i  4805  ssopr  4846  ideq  4870  coeq1i  4876  coeq2i  4877  cnveqi  4887  dmeqi  4908  dmv  4920  reseq1i  4930  reseq2i  4931  imaeq1i  4939  imaeq2i  4940  rneqi  4957  residm  4994  resdm  4998  resid  5005  ssrnres  5059  dmsnop  5069  cnvex  5102  dmex  5106  rnex  5107  cnviin  5118  funeqi  5128  funres  5143  funin  5163  funcnvres  5165  cnvresid  5166  fneq1i  5178  fneq2i  5179  fnresi  5200  dmopab2  5209  feq1i  5217  feq2i  5218  fdmi  5227  fssres  5238  fint  5245  foimacnv  5303  resdif  5306  resin  5307  f1ococnv2  5309  fveq1i  5329  fveq2i  5331  fv01  5354  fnressn  5438  fressnfv  5439  fvsnun1  5447  fvsnun2  5448  fconst2  5454  funiunfv  5467  isores1  5494  1stfo  5505  2ndfo  5506  swapf1o  5511  swapres  5512  opfv1st  5514  opfv2nd  5515  rnsi  5521  dmep  5524  oveq1i  5533  oveq2i  5534  oveqi  5536  oprabbii  5565  funoprab  5584  fnoprab  5586  fovcl  5588  ovidig  5593  ovigg  5596  caovmo  5645  dmmpti  5691  mpt2mpt  5709  fnmpt2i  5733  dmmpt2  5734  fixex  5789  ins2ex  5797  ins3ex  5798  imageex  5801  txpcofun  5803  brfns  5833  dmcross  5847  pw1fnval  5851  fnfullfun  5858  fullfunex  5860  fvfullfunlem3  5863  fvfullfun  5864  brfullfun  5866  dfnnc3  5885  eqerlem  5960  elqs  5977  ecqs  5988  map0  6025  mapsn  6026  enrflx  6035  dmen  6041  xpcomen  6052  xpassen  6057  enmap2lem3  6065  enmap1lem3  6071  enpw1pw  6075  enprmaplem3  6078  enprmaplem5  6080  enprmaplem6  6081  nceqi  6109  ncex  6117  nulnnc  6118  ncelncsi  6121  ncid  6123  eqnc  6127  1cnc  6139  df1c3  6140  ncaddccl  6144  ncdisjeq  6148  ncpw1c  6154  1p1e2c  6155  2p1e3c  6156  tc0c  6163  tcdi  6164  tc1c  6165  tc2c  6166  2nnc  6167  2nc  6168  ce0addcnnul  6179  ce0nnulb  6182  ce0nulnc  6184  ce2  6192  ce2nc1  6193  ce2ncpw11c  6194  lec0cg  6198  sbthlem1  6203  dflec2  6210  leconnnc  6218  ce2lt  6220  dflec3  6221  tcnc  6225  taddc  6229  letc  6231  ce2le  6233  cet  6234  tce2  6236  ce0lenc1  6239  brtcfn  6246  0lt1c  6258  nmembers1  6271  nncdiv3  6277  nchoicelem1  6289  nchoicelem5  6293  nchoicelem8  6296  nchoicelem9  6297  nchoicelem13  6301  nchoicelem17  6305  nchoicelem18  6306  nchoicelem19  6307  frecex  6313  frecxp  6314  fnfreclem2  6318  fnfreclem3  6319
 Copyright terms: Public domain W3C validator