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

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		wps	. . 3 wff 𝜓
3	2, 1	wi 4	. 2 wff (𝜓 → 𝜑)
4	1, 3	wi 4	1 wff (𝜑 → (𝜓 → 𝜑))

This axiom is referenced by:  a1i  9  id  19  idALT  20  a1d  22  a1dd  48  jarr  97  jarri  98  pm2.86i  99  pm2.86d  100  pm5.1im  173  biimt  241  pm5.4  249  pm4.45im  334  conax1  653  pm4.8  707  oibabs  714  imorr  721  pm2.53  722  imorri  749  jao1i  796  pm2.64  801  pm2.82  812  condcOLD  854  pm5.12dc  910  pm5.14dc  911  peircedc  914  pm4.83dc  951  dedlem0a  968  oplem1  975  stdpc4  1775  sbequi  1839  sbidm  1851  eumo  2058  moimv  2092  euim  2094  alral  2522  r19.12  2583  r19.27av  2612  r19.37  2629  gencbval  2786  eqvinc  2861  eqvincg  2862  rr19.3v  2877  ralidm  3524  ralm  3528  class2seteq  4164  exmid0el  4205  sotritric  4325  elnnnn0b  9220  zltnle  9299  iccneg  9989  qltnle  10246  frec2uzlt2d  10404  hashfzp1  10804  algcvgblem  12049  bj-trst  14494  bj-findis  14734