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  654  pm4.8  708  oibabs  715  imorr  722  pm2.53  723  imorri  750  jao1i  797  pm2.64  802  pm2.82  813  condcOLD  855  pm5.12dc  911  pm5.14dc  912  peircedc  915  pm4.83dc  953  dedlem0a  970  oplem1  977  stdpc4  1786  sbequi  1850  sbidm  1862  eumo  2074  moimv  2108  euim  2110  alral  2539  r19.12  2600  r19.27av  2629  r19.37  2646  gencbval  2808  eqvinc  2883  eqvincg  2884  rr19.3v  2899  ralidm  3547  ralm  3550  class2seteq  4192  exmid0el  4233  sotritric  4355  elnnnn0b  9284  zltnle  9363  iccneg  10055  qltnle  10313  frec2uzlt2d  10475  hashfzp1  10895  algcvgblem  12187  bj-trst  15231  bj-findis  15471