Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-1 GIF 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 𝜑 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  48  jarr  97  pm2.86i  98  pm2.86d  99  pm5.1im  172  biimt  240  pm5.4  248  pm4.45im  332  conax1  642  pm4.8  696  oibabs  703  imorr  710  pm2.53  711  imorri  738  jao1i  785  pm2.64  790  pm2.82  801  biort  814  condcOLD  839  pm5.12dc  895  pm5.14dc  896  peircedc  899  pm4.83dc  935  dedlem0a  952  oplem1  959  stdpc4  1748  sbequi  1811  sbidm  1823  eumo  2031  moimv  2065  euim  2067  alral  2478  r19.12  2538  r19.27av  2567  r19.37  2583  gencbval  2734  eqvinc  2808  eqvincg  2809  rr19.3v  2823  ralidm  3463  ralm  3467  class2seteq  4087  exmid0el  4127  sotritric  4246  elnnnn0b  9035  zltnle  9114  iccneg  9786  qltnle  10037  frec2uzlt2d  10191  hashfzp1  10584  algcvgblem  11743  bj-trst  13058  bj-findis  13284
 Copyright terms: Public domain W3C validator