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  659  pm4.8  715  oibabs  722  imorr  729  pm2.53  730  imorri  757  jao1i  804  pm2.64  809  pm2.82  820  condcOLD  862  pm5.12dc  918  pm5.14dc  919  peircedc  922  pm4.83dc  960  dedlem0a  977  oplem1  984  a1ddd  1481  stdpc4  1823  sbequi  1887  sbidm  1899  eumo  2111  moimv  2146  euim  2148  alral  2578  r19.12  2640  r19.27av  2669  r19.37  2686  gencbval  2853  eqvinc  2930  eqvincg  2931  rr19.3v  2946  ralidm  3597  ralm  3600  class2seteq  4259  exmid0el  4300  sotritric  4427  elnnnn0b  9505  zltnle  9586  iccneg  10285  qltnle  10566  frec2uzlt2d  10729  hashfzp1  11151  algcvgblem  12701  clwwlknonex2lem2  16379  bj-trst  16457  bj-findis  16695