Axiom ax-1 5

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  328  pm2.51  619  pm4.8  661  pm2.53  679  imorri  706  jao1i  748  pm2.64  753  pm2.82  764  biort  777  condc  790  imorr  838  oibabs  841  pm5.12dc  857  pm5.14dc  858  peircedc  861  pm4.83dc  900  dedlem0a  917  oplem1  924  stdpc4  1712  sbequi  1774  sbidm  1786  eumo  1987  moimv  2021  euim  2023  alral  2432  r19.12  2491  r19.27av  2518  r19.37  2533  gencbval  2681  eqvinc  2754  eqvincg  2755  rr19.3v  2769  ralidm  3402  ralm  3406  class2seteq  4019  exmid0el  4056  sotritric  4175  elnnnn0b  8815  zltnle  8894  iccneg  9555  qltnle  9806  frec2uzlt2d  9960  hashfzp1  10347  algcvgblem  11458  bj-findis  12582