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.

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  402  pm2.65i  547  notnoti  553  pm2.21i  554  pm2.24ii  555  notbii  573  nbn  594  ori  618  orci  626  olci  627  biorfi  641  imorri  644  notnotri  719  mt4  732  pm2.61i  743  simp1i  930  simp2i  931  simp3i  932  3jaoi  1209  merlem1  1252  merlem2  1253  merlem3  1254  merlem4  1255  merlem5  1256  merlem6  1257  merlem7  1258  merlem8  1259  merlem9  1260  merlem10  1261  merlem11  1262  merlem12  1263  merlem13  1264  luk-1  1265  luk-2  1266  luk-3  1267  luklem1  1268  luklem2  1269  luklem4  1271  luklem6  1273  luklem7  1274  luklem8  1275  ax2  1277  nic-mp  1287  nic-mpALT  1288  trud  1317  dfneg  1318  mpg  1341  19.23  1379  hbequid  1397  hbequidOLD  1398  equidqeOLD  1420  ax4  1423  ax5o  1424  ax5  1426  ax6  1429  a4i  1432  19.35i  1513  exan  1552  equid1  1561  hbae  1578  equvini  1602  equveli  1603  sbid  1618  sbie  1630  sbco  1690  sbidm  1692  a4eiv  1711  elsb3  1773  elsb4  1774  eubii  1838  mobii  1858  eumoi  1865  moani  1876
  Copyright terms: Public domain W3C validator