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 used 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  663  pm4.8  719  oibabs  726  imorr  733  pm2.53  734  imorri  761  jao1i  808  pm2.64  813  pm2.82  824  condcOLD  866  pm5.12dc  922  pm5.14dc  923  peircedc  926  pm4.83dc  964  dedlem0a  981  oplem1  988  a1ddd  1485  stdpc4  1828  sbequi  1892  sbidm  1904  eumo  2118  moimv  2153  euim  2155  alral  2595  r19.12  2657  r19.27av  2686  r19.37  2703  gencbval  2871  eqvinc  2949  eqvincg  2950  rr19.3v  2965  ralidm  3628  ralm  3631  class2seteq  4302  exmid0el  4343  sotritric  4471  elnnnn0b  9618  zltnle  9701  iccneg  10408  qltnle  10695  frec2uzlt2d  10862  hashfzp1  11287  algcvgblem  12852  bpos1  16310  clwwlknonex2lem2  16884  bj-trst  16972  bj-findis  17210