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

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  47  jarr  96  pm2.86i  97  pm2.86d  98  pm5.1im  171  biimt  239  pm5.4  247  pm4.45im  327  pm2.51  614  pm4.8  656  pm2.53  674  imorri  701  jao1i  743  pm2.64  748  pm2.82  759  biort  772  condc  783  imorr  831  oibabs  834  pm5.12dc  850  pm5.14dc  851  peircedc  854  pm4.83dc  893  dedlem0a  910  oplem1  917  stdpc4  1700  sbequi  1762  sbidm  1774  eumo  1975  moimv  2009  euim  2011  alral  2415  r19.12  2472  r19.27av  2498  r19.37  2512  gencbval  2658  eqvinc  2728  eqvincg  2729  rr19.3v  2743  ralidm  3363  ralm  3367  class2seteq  3963  exmid0el  3996  sotritric  4114  elnnnn0b  8608  zltnle  8691  iccneg  9300  qltnle  9545  frec2uzlt2d  9699  hashfzp1  10066  algcvgblem  10810  bj-findis  11216