ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-1 Unicode version

Axiom ax-1 5
Description: Axiom Simp. Axiom A1 of [Margaris] p. 49. One of the axioms of propositional calculus. This axiom is called Simp or "the principle of simplification" in Principia Mathematica (Theorem *2.02 of [WhiteheadRussell] p. 100) because "it enables us to pass from the joint assertion of  ph and  ps to the assertion of  ph simply."

The theorems of propositional calculus are also called tautologies. Although classical propositional logic tautologies can be proved using truth tables, there is no similarly simple system for intuitionistic propositional logic, so proving tautologies from axioms is the preferred approach. (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
ax-1  |-  ( ph  ->  ( ps  ->  ph )
)

Detailed syntax breakdown of Axiom ax-1
StepHypRef Expression
1 wph . 2  wff  ph
2 wps . . 3  wff  ps
32, 1wi 4 . 2  wff  ( ps 
->  ph )
41, 3wi 4 1  wff  ( ph  ->  ( ps  ->  ph )
)
Colors of variables: wff set class
This axiom is referenced by:  a1i  9  id  19  idALT  20  a1d  22  a1dd  46  jarr  95  pm2.86i  96  pm2.86d  97  pm5.1im  166  biimt  234  pm5.4  242  pm4.45im  321  pm2.51  591  pm4.8  633  pm2.53  651  imorri  678  jao1i  720  pm2.64  725  pm2.82  736  biort  749  condc  760  imorr  808  oibabs  811  pm5.12dc  827  pm5.14dc  828  peircedc  831  pm4.83dc  869  dedlem0a  886  oplem1  893  stdpc4  1674  sbequi  1736  sbidm  1747  eumo  1948  moimv  1982  euim  1984  alral  2384  r19.12  2439  r19.27av  2465  r19.37  2479  gencbval  2619  eqvinc  2689  eqvincg  2690  rr19.3v  2704  ralidm  3348  ralm  3352  class2seteq  3943  sotritric  4088  elnnnn0b  8282  zltnle  8347  iccneg  8957  qltnle  9202  frec2uzlt2d  9353  algcvgblem  10250  bj-findis  10470
  Copyright terms: Public domain W3C validator