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  47  jarr  96  pm2.86i  97  pm2.86d  98  pm5.1im  171  biimt  239  pm5.4  247  pm4.45im  327  pm2.51  614  pm4.8  656  pm2.53  674  imorri  701  jao1i  743  pm2.64  748  pm2.82  759  biort  772  condc  783  imorr  831  oibabs  834  pm5.12dc  850  pm5.14dc  851  peircedc  854  pm4.83dc  893  dedlem0a  910  oplem1  917  stdpc4  1700  sbequi  1762  sbidm  1774  eumo  1975  moimv  2009  euim  2011  alral  2414  r19.12  2471  r19.27av  2497  r19.37  2511  gencbval  2656  eqvinc  2726  eqvincg  2727  rr19.3v  2741  ralidm  3358  ralm  3362  class2seteq  3957  exmid0el  3989  sotritric  4107  elnnnn0b  8451  zltnle  8530  iccneg  9139  qltnle  9384  frec2uzlt2d  9538  hashfzp1  9900  algcvgblem  10638  bj-findis  11041
  Copyright terms: Public domain W3C validator