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  621  orci  629  olci  630  biorfi  644  imorri  647  simp1i  871  simp2i  872  simp3i  873  3jaoi  1151  trud  1199  dfnot  1208  mpto1  1252  mtp-xor  1254  mtp-or  1255  mpg  1277  19.23  1325  hbequid  1345  nfri  1350  equidqeOLD  1364  spi  1368  19.21  1412  eximii  1429  19.35i  1451  19.37aiv  1491  exan  1506  equid  1511  hbae  1528  equvini  1563  equveli  1564  sbid  1579  sbieh  1594  exdistrf  1602  dveeq2or  1618  ax11v  1629  ax11ev  1630  equs5or  1632  sb4or  1635  sb4bor  1637  nfsb2or  1639  sbequilem  1640  sbequi  1641  speiv  1663  nfsbxy  1735  nfsbxyt  1736  sbco  1759  sbcocom  1761  sbcomxyyz  1763  elsb3  1769  elsb4  1770  sbal1yz  1794  dvelimALT  1801  dvelimfv  1802  dvelimor  1809  eumoi  1846  moani  1882  eqeq1i  1934  eqeq2i  1937  eleq1i  1990  eleq2i  1991  nfcrii  2056  neeq1i  2099  neeq2i  2100  necon3i  2128  rspec  2242  rgen2a  2244  mprg  2247  r19.21  2264  r19.23  2293  raleqi  2375  rexeqi  2376  elexi  2432  ceqsal  2448  vtocl3  2475  vtoclef  2491  vtocle  2492  spcv  2511  spcev  2512  clel3  2543  elabf  2550  elab2  2554  elab3  2558  euxfrdc  2589  reueq  2600  rmoimi2  2604  sbsbc  2630  sbc8g  2633  sbc6  2651  sbcie  2659  csbvarg  2742  csbief  2756  csbie2  2760  sbnfc2  2773  sseli  2808  sselii  2809  sseq1i  2836  sseq2i  2837  psseq1i  2900  psseq2i  2901  difeq1i  2925  difeq2i  2926  pm2.61i  2960
  Copyright terms: Public domain W3C validator