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  643  pm4.8  697  oibabs  704  imorr  711  pm2.53  712  imorri  739  jao1i  786  pm2.64  791  pm2.82  802  condcOLD  844  pm5.12dc  900  pm5.14dc  901  peircedc  904  pm4.83dc  941  dedlem0a  958  oplem1  965  stdpc4  1763  sbequi  1827  sbidm  1839  eumo  2046  moimv  2080  euim  2082  alral  2510  r19.12  2571  r19.27av  2600  r19.37  2617  gencbval  2773  eqvinc  2848  eqvincg  2849  rr19.3v  2864  ralidm  3508  ralm  3512  class2seteq  4141  exmid0el  4182  sotritric  4301  elnnnn0b  9154  zltnle  9233  iccneg  9921  qltnle  10177  frec2uzlt2d  10335  hashfzp1  10733  algcvgblem  11977  bj-trst  13580  bj-findis  13821