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  pm2.86i  98  pm2.86d  99  pm5.1im  172  biimt  240  pm5.4  248  pm4.45im  332  conax1  648  pm4.8  702  oibabs  709  imorr  716  pm2.53  717  imorri  744  jao1i  791  pm2.64  796  pm2.82  807  condcOLD  849  pm5.12dc  905  pm5.14dc  906  peircedc  909  pm4.83dc  946  dedlem0a  963  oplem1  970  stdpc4  1768  sbequi  1832  sbidm  1844  eumo  2051  moimv  2085  euim  2087  alral  2515  r19.12  2576  r19.27av  2605  r19.37  2622  gencbval  2778  eqvinc  2853  eqvincg  2854  rr19.3v  2869  ralidm  3515  ralm  3519  class2seteq  4149  exmid0el  4190  sotritric  4309  elnnnn0b  9179  zltnle  9258  iccneg  9946  qltnle  10202  frec2uzlt2d  10360  hashfzp1  10759  algcvgblem  12003  bj-trst  13774  bj-findis  14014