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  711  oibabs  718  imorr  725  pm2.53  726  imorri  753  jao1i  800  pm2.64  805  pm2.82  816  condcOLD  858  pm5.12dc  914  pm5.14dc  915  peircedc  918  pm4.83dc  956  dedlem0a  973  oplem1  980  a1ddd  1458  stdpc4  1801  sbequi  1865  sbidm  1877  eumo  2089  moimv  2124  euim  2126  alral  2555  r19.12  2617  r19.27av  2646  r19.37  2663  gencbval  2829  eqvinc  2906  eqvincg  2907  rr19.3v  2922  ralidm  3572  ralm  3575  class2seteq  4226  exmid0el  4267  sotritric  4392  elnnnn0b  9381  zltnle  9460  iccneg  10153  qltnle  10430  frec2uzlt2d  10593  hashfzp1  11013  algcvgblem  12537  bj-trst  16013  bj-findis  16252