ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-mp Structured version   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  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  1147  trud  1195  dfnot  1204  mpto1  1247  mtp-xor  1249  mtp-or  1250  mpg  1272  19.23  1320  hbequid  1340  nfri  1345  equidqeOLD  1359  a4i  1363  19.21  1408  eximii  1424  19.35i  1446  19.37aiv  1483  exan  1498  equid  1503  hbae  1519  equvini  1551  equveli  1552  sbid  1568  sbieh  1583  exdistrf  1591  sbcof2  1601  dveeq2or  1607  ax11v  1618  ax11ev  1619  equs5or  1621  sb4or  1624  sb4bor  1626  nfsb2or  1628  sbequilem  1629  sbequi  1630  a4eiv  1651  nfsbxy  1724  nfsbxyt  1725  sbco  1748  sbcocom  1750  sbcomxyyz  1752  elsb3  1758  elsb4  1759  sbal1yz  1783  dvelimALT  1790  dvelimfv  1791  dvelimor  1798  eumoi  1833  eqeq1i  1874  eqeq2i  1877  eleq1i  1930  eleq2i  1931  nfcrii  1996  neeq1i  2039  neeq2i  2040  necon3i  2068  rspec  2182  rgen2a  2184  mprg  2187  r19.21  2204  r19.23  2233  raleqi  2314  rexeqi  2315  elexi  2370  ceqsal  2386  vtocl3  2413  vtoclef  2429  vtocle  2430  spcv  2449  spcev  2450  clel3  2481  elabf  2488  elab2  2492  elab3  2496  pm2.61i  2521  moani  2565
  Copyright terms: Public domain W3C validator