ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-1 Unicode version

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
StepHypRef Expression
1 wph . 2  wff  ph
2 wps . . 3  wff  ps
32, 1wi 4 . 2  wff  ( ps 
->  ph )
41, 3wi 4 1  wff  ( ph  ->  ( ps  ->  ph )
)
Colors of variables: wff set class
This axiom is referenced by:  a1i  9  id  19  idALT  20  a1d  22  a1dd  47  jarr  96  pm2.86i  97  pm2.86d  98  pm5.1im  171  biimt  239  pm5.4  247  pm4.45im  327  pm2.51  614  pm4.8  656  pm2.53  674  imorri  701  jao1i  743  pm2.64  748  pm2.82  759  biort  772  condc  785  imorr  833  oibabs  836  pm5.12dc  852  pm5.14dc  853  peircedc  856  pm4.83dc  895  dedlem0a  912  oplem1  919  stdpc4  1702  sbequi  1764  sbidm  1776  eumo  1977  moimv  2011  euim  2013  alral  2417  r19.12  2474  r19.27av  2500  r19.37  2515  gencbval  2661  eqvinc  2731  eqvincg  2732  rr19.3v  2746  ralidm  3369  ralm  3373  class2seteq  3973  exmid0el  4007  sotritric  4125  elnnnn0b  8650  zltnle  8729  iccneg  9338  qltnle  9585  frec2uzlt2d  9739  hashfzp1  10129  algcvgblem  10913  bj-findis  11319
  Copyright terms: Public domain W3C validator