Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-mp GIF 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 wff ψ
 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  746  simp1i  878  simp2i  879  simp3i  880  3jaoi  1157  trud  1205  dfnot  1214  mpto1  1246  mtp-xor  1248  mtp-or  1249  mpg  1271  19.23  1319  hbequid  1339  nfri  1344  equidqeOLD  1356  a4i  1360  19.35i  1427  exan  1470  equid  1475  hbae  1491  equvini  1517  equveli  1518  sbid  1536  sbie  1549  exdistrf  1556  sbcof2  1566  dveeq2or  1572  ax11v  1583  ax11ev  1584  equs5or  1586  sb4or  1589  sb4bor  1591  nfsb2or  1593  sbequilem  1594  sbequi  1595  a4eiv  1614  nfsbxy  1684  sbco  1706  sbcocom  1708  sbcomxyyz  1710  elsb3  1714  elsb4  1715  sbal1yz  1739  dvelimALT  1746  dvelimfv  1747  eubii  1775  mobii  1795  eumoi  1802  moani  1813  notnotri  1852  ax5o  1912  ax5  1914  ax4  1915
 Copyright terms: Public domain W3C validator