ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-1 GIF 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 𝜑 and 𝜓 to the assertion of 𝜑 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 (𝜑 → (𝜓𝜑))

Detailed syntax breakdown of Axiom ax-1
StepHypRef Expression
1 wph . 2 wff 𝜑
2 wps . . 3 wff 𝜓
32, 1wi 4 . 2 wff (𝜓𝜑)
41, 3wi 4 1 wff (𝜑 → (𝜓𝜑))
Colors of variables: wff set class
This axiom is referenced by:  a1i  9  id  19  idALT  20  a1d  22  a1dd  42  jarr  91  pm2.86i  92  pm2.86d  93  pm5.1im  162  biimt  230  pm5.4  238  pm4.45im  317  pm2.51  581  pm4.8  623  pm2.53  641  imorri  668  pm2.64  714  pm2.82  725  biort  738  condc  749  imorr  797  oibabs  800  pm5.12dc  816  pm5.14dc  817  peircedc  820  pm4.83dc  858  dedlem0a  875  oplem1  882  stdpc4  1658  sbequi  1720  sbidm  1731  eumo  1932  moimv  1966  euim  1968  alral  2364  r19.12  2419  r19.27av  2445  r19.37  2459  gencbval  2599  eqvinc  2664  eqvincg  2665  rr19.3v  2679  ralidm  3318  ralm  3322  class2seteq  3913  sotritric  4058  elnnnn0b  8189  zltnle  8254  iccneg  8815  frec2uzlt2d  9059  algcvgblem  9756  bj-findis  9968
  Copyright terms: Public domain W3C validator