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 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
Colors of variables: wff set class
This axiom is referenced by:  mp2b  8  a1i  9  a2i  10  mpd  12  mp2  15  id1  18  simpli  102  simpri  104  biimpi  111  bicomi  121  mpbi  131  mpbir  132  imbi1i  225  a1bi  230  tbt  234  biantru  284  biantrur  285  mp2an  400  pm2.65i  546  notnoti  552  pm2.21i  553  pm2.24ii  554  notbii  572  nbn  593  ori  617  orci  625  olci  626  biorfi  640  imorri  643  pm2.61i  737  simp1i  869  simp2i  870  simp3i  871  3jaoi  1148  trud  1196  dfneg  1197  mpg  1220  19.23  1258  hbequid  1276  equidqeOLD  1285  ax5o  1287  ax5  1289  ax6  1292  a4i  1295  19.35i  1355  exan  1386  equid  1392  hbae  1408  equvini  1434  equveli  1435  sbid  1450  sbie  1462  sbcof2  1477  sbco  1529  sbidm  1531  a4eiv  1546  ax11v  1569  ax11ev  1570  sbcov  1578  elsb3  1614  elsb4  1615  eubii  1678  mobii  1698  eumoi  1705  moani  1716  notnotri  1755  ax4  1808
  Copyright terms: Public domain W3C validator