![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ax-1 | GIF version |
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.) |
Ref | Expression |
---|---|
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 (𝜑 → (𝜓 → 𝜑)) |
Colors of variables: wff set class |
This axiom is referenced by: a1i 9 id 19 idALT 20 a1d 22 a1dd 48 jarr 97 jarri 98 pm2.86i 99 pm2.86d 100 pm5.1im 173 biimt 241 pm5.4 249 pm4.45im 334 conax1 654 pm4.8 708 oibabs 715 imorr 722 pm2.53 723 imorri 750 jao1i 797 pm2.64 802 pm2.82 813 condcOLD 855 pm5.12dc 911 pm5.14dc 912 peircedc 915 pm4.83dc 953 dedlem0a 970 oplem1 977 stdpc4 1786 sbequi 1850 sbidm 1862 eumo 2070 moimv 2104 euim 2106 alral 2535 r19.12 2596 r19.27av 2625 r19.37 2642 gencbval 2800 eqvinc 2875 eqvincg 2876 rr19.3v 2891 ralidm 3538 ralm 3542 class2seteq 4181 exmid0el 4222 sotritric 4342 elnnnn0b 9251 zltnle 9330 iccneg 10021 qltnle 10278 frec2uzlt2d 10437 hashfzp1 10839 algcvgblem 12084 bj-trst 14969 bj-findis 15209 |
Copyright terms: Public domain | W3C validator |