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  657  pm4.8  712  oibabs  719  imorr  726  pm2.53  727  imorri  754  jao1i  801  pm2.64  806  pm2.82  817  condcOLD  859  pm5.12dc  915  pm5.14dc  916  peircedc  919  pm4.83dc  957  dedlem0a  974  oplem1  981  a1ddd  1478  stdpc4  1821  sbequi  1885  sbidm  1897  eumo  2109  moimv  2144  euim  2146  alral  2575  r19.12  2637  r19.27av  2666  r19.37  2683  gencbval  2850  eqvinc  2927  eqvincg  2928  rr19.3v  2943  ralidm  3593  ralm  3596  class2seteq  4249  exmid0el  4290  sotritric  4417  elnnnn0b  9434  zltnle  9513  iccneg  10212  qltnle  10491  frec2uzlt2d  10654  hashfzp1  11075  algcvgblem  12608  clwwlknonex2lem2  16223  bj-trst  16245  bj-findis  16484