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  613  pm4.8  655  pm2.53  673  imorri  700  jao1i  742  pm2.64  747  pm2.82  758  biort  771  condc  782  imorr  830  oibabs  833  pm5.12dc  849  pm5.14dc  850  peircedc  853  pm4.83dc  892  dedlem0a  909  oplem1  916  stdpc4  1698  sbequi  1760  sbidm  1772  eumo  1973  moimv  2007  euim  2009  alral  2409  r19.12  2466  r19.27av  2492  r19.37  2506  gencbval  2647  eqvinc  2718  eqvincg  2719  rr19.3v  2733  ralidm  3341  ralm  3345  class2seteq  3937  sotritric  4079  elnnnn0b  8332  zltnle  8397  iccneg  9011  qltnle  9255  frec2uzlt2d  9406  algcvgblem  10431  bj-findis  10774