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 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  id1  20  a1d  22  a1dd  42  jarr  91  pm2.86i  92  pm2.86d  93  pm5.1im  162  biimt  230  pm5.4  238  pm4.45im  317  pm2.51  580  pm4.8  622  pm2.53  640  imorri  667  pm2.64  713  pm2.82  724  biort  737  condc  748  imorr  796  oibabs  799  pm5.12dc  815  pm5.14dc  816  peircedc  819  pm4.83dc  857  dedlem0a  874  oplem1  881  stdpc4  1655  sbequi  1717  sbidm  1728  eumo  1929  moimv  1963  euim  1965  alral  2361  r19.12  2416  r19.27av  2442  r19.37  2456  gencbval  2596  eqvinc  2661  eqvincg  2662  rr19.3v  2676  ralidm  3315  ralm  3319  class2seteq  3907  sotritric  4052  elnnnn0b  8002  zltnle  8067  iccneg  8627  frec2uzlt2d  8871  bj-findis  9439