ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-mp GIF 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.

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  9  a1i  10  a2i  11  mpd  13  mp2  16  id1  19  simpli  103  simpri  105  biimpi  112  bicomi  122  mpbi  132  mpbir  133  imbi1i  226  a1bi  231  tbt  235  biantru  285  biantrur  286  mp2an  401  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  736  simp1i  886  simp2i  887  simp3i  888  3jaoi  1165  trud  1213  dfneg  1214  mpg  1237  19.23  1275  hbequid  1293  equidqeOLD  1302  ax5o  1304  ax5  1306  ax6  1309  a4i  1312  19.35i  1373  exan  1406  equid  1413  hbae  1429  equvini  1455  equveli  1456  sbid  1471  sbie  1483  sbcof2  1498  sbco  1550  sbidm  1552  a4eiv  1567  ax11v  1590  sbcov  1598  elsb3  1636  elsb4  1637  eubii  1697  mobii  1717  eumoi  1724  moani  1735  notnotri  1774  ax4  1809
  Copyright terms: Public domain W3C validator