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

Axiom ax-1 6
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  48  jarr  97  pm2.86i  98  pm2.86d  99  pm5.1im  172  biimt  240  pm5.4  248  pm4.45im  332  conax1  627  pm4.8  681  oibabs  688  imorr  695  pm2.53  696  imorri  723  jao1i  770  pm2.64  775  pm2.82  786  biort  799  condcOLD  824  pm5.12dc  880  pm5.14dc  881  peircedc  884  pm4.83dc  920  dedlem0a  937  oplem1  944  stdpc4  1733  sbequi  1795  sbidm  1807  eumo  2009  moimv  2043  euim  2045  alral  2455  r19.12  2515  r19.27av  2544  r19.37  2560  gencbval  2708  eqvinc  2782  eqvincg  2783  rr19.3v  2797  ralidm  3433  ralm  3437  class2seteq  4057  exmid0el  4097  sotritric  4216  elnnnn0b  8979  zltnle  9058  iccneg  9727  qltnle  9978  frec2uzlt2d  10132  hashfzp1  10525  algcvgblem  11642  bj-trst  12847  bj-findis  13073
  Copyright terms: Public domain W3C validator