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 ph and ps to the assertion of ph 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	|- ( ph -> ( ps -> ph ) )

Detailed syntax breakdown of Axiom ax-1

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		wps	. . 3 wff ps
3	2, 1	wi 4	. 2 wff ( ps -> ph )
4	1, 3	wi 4	1 wff ( ph -> ( ps -> ph ) )

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  biort  815  condcOLD  840  pm5.12dc  896  pm5.14dc  897  peircedc  900  pm4.83dc  936  dedlem0a  953  oplem1  960  stdpc4  1749  sbequi  1812  sbidm  1824  eumo  2032  moimv  2066  euim  2068  alral  2481  r19.12  2541  r19.27av  2570  r19.37  2586  gencbval  2737  eqvinc  2812  eqvincg  2813  rr19.3v  2827  ralidm  3468  ralm  3472  class2seteq  4095  exmid0el  4135  sotritric  4254  elnnnn0b  9045  zltnle  9124  iccneg  9802  qltnle  10054  frec2uzlt2d  10208  hashfzp1  10602  algcvgblem  11766  bj-trst  13122  bj-findis  13348