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  655  pm4.8  709  oibabs  716  imorr  723  pm2.53  724  imorri  751  jao1i  798  pm2.64  803  pm2.82  814  condcOLD  856  pm5.12dc  912  pm5.14dc  913  peircedc  916  pm4.83dc  954  dedlem0a  971  oplem1  978  a1ddd  1456  stdpc4  1799  sbequi  1863  sbidm  1875  eumo  2087  moimv  2121  euim  2123  alral  2552  r19.12  2613  r19.27av  2642  r19.37  2659  gencbval  2822  eqvinc  2897  eqvincg  2898  rr19.3v  2913  ralidm  3562  ralm  3565  class2seteq  4211  exmid0el  4252  sotritric  4375  elnnnn0b  9346  zltnle  9425  iccneg  10118  qltnle  10393  frec2uzlt2d  10556  hashfzp1  10976  algcvgblem  12415  bj-trst  15749  bj-findis  15989