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  714  oibabs  721  imorr  728  pm2.53  729  imorri  756  jao1i  803  pm2.64  808  pm2.82  819  condcOLD  861  pm5.12dc  917  pm5.14dc  918  peircedc  921  pm4.83dc  959  dedlem0a  976  oplem1  983  a1ddd  1480  stdpc4  1823  sbequi  1887  sbidm  1899  eumo  2111  moimv  2146  euim  2148  alral  2577  r19.12  2639  r19.27av  2668  r19.37  2685  gencbval  2852  eqvinc  2929  eqvincg  2930  rr19.3v  2945  ralidm  3595  ralm  3598  class2seteq  4253  exmid0el  4294  sotritric  4421  elnnnn0b  9445  zltnle  9524  iccneg  10223  qltnle  10502  frec2uzlt2d  10665  hashfzp1  11087  algcvgblem  12620  clwwlknonex2lem2  16288  bj-trst  16335  bj-findis  16574