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  notnotri  718  mt4  731  pm2.61i  742  simp1i  909  simp2i  910  simp3i  911  3jaoi  1188  trud  1235  dfneg  1236  mpg  1259  19.23  1297  hbequid  1315  equidqeOLD  1324  ax4  1326  ax5o  1327  ax5  1329  ax6  1332  a4i  1335  19.35i  1397  exan  1432  equid1  1440  hbae  1457  equvini  1481  equveli  1482  sbid  1497  sbie  1509  sbco  1569  sbidm  1571  a4eiv  1590  elsb3  1652  elsb4  1653  eubii  1699  mobii  1719  eumoi  1726  moani  1737
  Copyright terms: Public domain W3C validator