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  549  notnoti  555  pm2.21i  556  pm2.24ii  557  notbii  575  nbn  596  ori  620  orci  628  olci  629  biorfi  643  imorri  646  simp1i  867  simp2i  868  simp3i  869  3jaoi  1146  trud  1194  dfnot  1203  mpto1  1246  mtp-xor  1248  mtp-or  1249  mpg  1271  19.23  1319  hbequid  1339  nfri  1344  equidqeOLD  1357  a4i  1361  19.35i  1431  exan  1475  equid  1480  hbae  1496  equvini  1525  equveli  1526  sbid  1544  sbieh  1559  exdistrf  1567  sbcof2  1577  dveeq2or  1583  ax11v  1594  ax11ev  1595  equs5or  1597  sb4or  1600  sb4bor  1602  nfsb2or  1604  sbequilem  1605  sbequi  1606  a4eiv  1625  nfsbxy  1695  nfsbxyt  1696  sbco  1719  sbcocom  1721  sbcomxyyz  1723  elsb3  1729  elsb4  1730  sbal1yz  1754  dvelimALT  1761  dvelimfv  1762  dvelimor  1769  eqeq1i  1799  eqeq2i  1802  eleq1i  1855  eleq2i  1856  nfcrii  1921  neeq1i  1964  neeq2i  1965  necon3i  1993  pm2.61i  2048  eubii  2084  mobii  2104  eumoi  2111  moani  2122
  Copyright terms: Public domain W3C validator