Type  Label  Description 
Statement 

Theorem  pm3.2ni 701 
Infer negated disjunction of negated premises.



Theorem  orabs 702 
Absorption of redundant internal disjunct. Compare Theorem *4.45 of
[WhiteheadRussell] p. 119. (The
proof was shortened by Wolf Lammen,
28Feb2014.)



Theorem  orabsOLD 703 
Obsolete proof of orabs 702 as of 28Feb2014.



Theorem  oranabs 704 
Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton
23Jun2005.) (The proof was shortened by Wolf Lammen, 10Nov2013.)



Theorem  ordi 705 
Distributive law for disjunction. Theorem *4.41 of [WhiteheadRussell]
p. 119. (Revised by Mario Carneiro, 31Jan2015.)



Theorem  ordir 706 
Distributive law for disjunction.



Theorem  andi 707 
Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell]
p. 118. (The proof was shortened by Wolf Lammen, 5Jan2013.)



Theorem  andir 708 
Distributive law for conjunction.



Theorem  orddi 709 
Double distributive law for disjunction.



Theorem  anddi 710 
Double distributive law for conjunction.



Theorem  pm4.39 711 
Theorem *4.39 of [WhiteheadRussell] p.
118.



Theorem  pm4.72 712 
Implication in terms of biconditional and disjunction. Theorem *4.72 of
[WhiteheadRussell] p. 121. (The
proof was shortened by Wolf Lammen,
30Jan2013.)



Theorem  pm5.16 713 
Theorem *5.16 of [WhiteheadRussell] p.
124.
(Revised by Mario Carneiro, 31Jan2015.)



Theorem  biort 714 
A wff is disjoined with truth is true.



1.2.7 Classical logic


Theorem  con4d 715 
Deduction derived from axiom ax3 7.



Theorem  pm2.18 716 
Proof by contradiction. Theorem *2.18 of [WhiteheadRussell] p. 103. Also
called the Law of Clavius.



Theorem  pm2.18d 717 
Deduction based on reductio ad absurdum. (Contributed by FL,
12Jul2009.) (The proof was shortened by Andrew Salmon,
7May2011.)



Theorem  notnot2 718 
Converse of double negation. Theorem *2.14 of [WhiteheadRussell] p. 102.
(The proof was shortened by David Harvey, 5Sep1999. An even shorter
proof found by Josh Purinton, 29Dec2000.)



Theorem  notnotri 719 
Inference from double negation.



Theorem  con1d 720 
A contraposition deduction.



Theorem  con1 721 
Contraposition. Theorem *2.15 of [WhiteheadRussell] p. 102. (The proof
was shortened by Wolf Lammen, 12Feb2013.)



Theorem  mt3d 722 
Modus tollens deduction.



Theorem  mt3i 723 
Modus tollens inference. (The proof was shortened by Wolf Lammen,
15Sep2012.)



Theorem  mt3 724 
A rule similar to modus tollens. (The proof was shortened by Wolf
Lammen, 11Sep2013.)



Theorem  nsyl2 725 
A negated syllogism inference.



Theorem  con1i 726 
A contraposition inference. (The proof was shortened by O'Cat,
28Nov2008.) (The proof was shortened by Wolf Lammen, 19Jun2013.)



Theorem  nsyl4 727 
A negated syllogism inference.



Theorem  con4i 728 
Inference rule derived from axiom ax3 7. (The proof was shortened by
Wolf Lammen, 21Jun2013.)



Theorem  impi 729 
An importation inference. (The proof was shortened by Wolf Lammen,
20Jul2013.)



Theorem  simprim 730 
Simplification. Similar to Theorem *3.27 (Simp) of [WhiteheadRussell]
p. 112. (The proof was shortened by Wolf Lammen, 13Nov2012.)



Theorem  simplim 731 
Simplification. Similar to Theorem *3.26 (Simp) of [WhiteheadRussell]
p. 112. (The proof was shortened by Wolf Lammen, 21Jul2012.)



Theorem  mt4 732 
The rule of modus tollens. (Contributed by Wolf Lammen,
12May2013.)



Theorem  mt4d 733 
Modus tollens deduction.



Theorem  mt4i 734 
Modus tollens inference. (Contributed by Wolf Lammen, 12May2013.)



Theorem  pm2.61d 735 
Deduction eliminating an antecedent. (The proof was shortened by Wolf
Lammen, 12Sep2013.)



Theorem  pm2.61d1 736 
Inference eliminating an antecedent.



Theorem  pm2.61d2 737 
Inference eliminating an antecedent.



Theorem  ja 738 
Inference joining the antecedents of two premises. (The proof was
shortened by O'Cat, 19Feb2008.)



Theorem  jad 739 
Deduction form of ja 738. (Contributed by Scott Fenton, 13Dec2010.)
(The proof was shortened by Andrew Salmon, 17Sep2011.)



Theorem  peirce 740 
Peirce's axiom. This oddlooking theorem is the "difference" between
an
intuitionistic system of propositional calculus and a classical system and
is not accepted by intuitionists. When Peirce's axiom is added to an
intuitionistic system, the system becomes equivalent to our classical
system ax1 5 through ax3 7. A curious fact about this theorem is
that
it requires ax3 7 for its proof even though the result has no
negation
connectives in it. (The proof was shortened by Wolf Lammen,
9Oct2012.)



Theorem  pm2.6 741 
Theorem *2.6 of [WhiteheadRussell] p.
107.



Theorem  pm2.61 742 
Theorem *2.61 of [WhiteheadRussell] p.
107. Useful for eliminating an
antecedent. (The proof was shortened by Wolf Lammen, 22Sep2013.)



Theorem  pm2.61i 743 
Inference eliminating an antecedent. (The proof was shortened by Wolf
Lammen, 12Sep2013.)



Theorem  pm2.61ii 744 
Inference eliminating two antecedents. (The proof was shortened by Josh
Purinton, 29Dec2000.)



Theorem  pm2.61ian 745 
Elimination of an antecedent.



Theorem  pm2.61dan 746 
Elimination of an antecedent.



Theorem  pm2.61ddan 747 
Elimination of two antecedents.



Theorem  pm2.61dda 748 
Elimination of two antecedents.



Theorem  pm2.61nii 749 
Inference eliminating two antecedents. (The proof was shortened by
Andrew Salmon, 25May2011.) (The proof was shortened by Wolf Lammen,
13Nov2012.)



Theorem  pm2.61iii 750 
Inference eliminating three antecedents. (The proof was shortened by
Wolf Lammen, 22Sep2013.)



Theorem  impt 751 
Importation theorem expressed with primitive connectives. (The proof was
shortened by Wolf Lammen, 20Jul2013.)



Theorem  impcon4bid 752 
A variation on impbid 119 with contraposition. (Contributed by Jeff
Hankins, 3Jul2009.)



Theorem  pm2.5 753 
Theorem *2.5 of [WhiteheadRussell] p.
107. (The proof was shortened by
Wolf Lammen, 9Oct2012.)



Theorem  pm2.521 754 
Theorem *2.521 of [WhiteheadRussell]
p. 107. (The proof was shortened by
Wolf Lammen, 8Oct2012.)



Theorem  loolin 755 
The Linearity Axiom of the infinitevalued sentential logic (Linfinity)
of Lukasiewicz. For a version not using ax3 7,
see loolinALT 94.
(Contributed by O'Cat, 12Aug2004.) (The proof was shortened by Wolf
Lammen, 2Nov2012.)



Theorem  looinv 756 
The Inversion Axiom of the infinitevalued sentential logic (Linfinity)
of Lukasiewicz. Using dfor2 794, we can see that this essentially
expresses "disjunction commutes." Theorem *2.69 of [WhiteheadRussell]
p. 108.



Theorem  con34b 757 
Contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116.



Theorem  notnot 758 
Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117.



Theorem  con4bid 759 
A contraposition deduction.



Theorem  notbi 760 
Contraposition. Theorem *4.11 of [WhiteheadRussell] p. 117. (The proof
was shortened by Wolf Lammen, 12Jun2013.)



Theorem  con2bi 761 
Contraposition. Theorem *4.12 of [WhiteheadRussell] p. 117. (The proof
was shortened by Wolf Lammen, 3Jan2013.)



Theorem  con2bid 762 
A contraposition deduction.



Theorem  con1bid 763 
A contraposition deduction.



Theorem  con1bii 764 
A contraposition inference. (The proof was shortened by Wolf Lammen,
13Oct2012.)



Theorem  con1biiOLD 765 
Obsolete proof of con1bii 764 as of 28Sep2014.



Theorem  con1b 766 
Contraposition. Bidirectional version of con1 721.



Theorem  con4bii 767 
A contraposition inference.



Theorem  con2bii 768 
A contraposition inference.



Theorem  bija 769 
Combine antecedents into a single biconditional. This inference,
reminiscent of ja 738, is reversible: The hypotheses can be deduced
from
the conclusion alone (see pm5.1im 161 and pm5.21im 591). (Contributed by
Wolf Lammen, 13May2013.)



Theorem  pm5.18 770 
Theorem *5.18 of [WhiteheadRussell] p.
124. This theorem says that
logical equivalence is the same as negated "exclusiveor." (The
proof was
shortened by Andrew Salmon, 20Jun2011.) (The proof was shortened by
Wolf Lammen, 15Oct2013.)



Theorem  xor3 771 
Two ways to express "exclusive or."



Theorem  nbbn 772 
Move negation outside of biconditional. Compare Theorem *5.18 of
[WhiteheadRussell] p. 124. (The
proof was shortened by Wolf Lammen,
20Sep2013.)



Theorem  biass 773 
Associative law for the biconditional. An axiom of system DS in Vladimir
Lifschitz, "On calculational proofs", Annals of Pure and Applied
Logic,
113:207224, 2002,
http://www.cs.utexas.edu/users/ailab/pubview.php?PubID=26805.
Interestingly, this law was not included in Principia Mathematica
but
was apparently first noted by Jan Lukasiewicz circa 1923. (The proof was
shortened by Juha Arpiainen, 19Jan2006.) (The proof was shortened by
Wolf Lammen, 21Sep2013.)



Theorem  pm4.81 774 
Theorem *4.81 of [WhiteheadRussell] p.
122.



Theorem  dfan 775 
Definition of 'and' in terms of negation and implication (classical).



Theorem  pm4.63 776 
Theorem *4.63 of [WhiteheadRussell] p.
120.



Theorem  pm4.67 777 
Theorem *4.67 of [WhiteheadRussell] p.
120.



Theorem  dfbi1 778 
Relate the biconditional connective to primitive connectives.



Theorem  iman 779 
Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll]
p. 176. (The proof was shortened by Wolf Lammen, 30Oct2012.)



Theorem  annim 780 
Express conjunction in terms of implication.



Theorem  pm4.61 781 
Theorem *4.61 of [WhiteheadRussell] p.
120.



Theorem  pm4.65 782 
Theorem *4.65 of [WhiteheadRussell] p.
120.



Theorem  pm4.14 783 
Theorem *4.14 of [WhiteheadRussell] p.
117. (The proof was shortened by
Wolf Lammen, 23Oct2012.)



Theorem  pm3.37 784 
Theorem *3.37 (Transp) of [WhiteheadRussell] p. 112. (The proof was
shortened by Wolf Lammen, 23Oct2012.)



Theorem  pm4.15 785 
Theorem *4.15 of [WhiteheadRussell] p.
117. (The proof was shortened by
Wolf Lammen, 18Nov2012.)



Theorem  condan 786 
Proof by contradiction. (The proof was shortened by Wolf Lammen,
19Jun2014.)



Theorem  xordi 787 
Conjunction distributes over exclusiveor, using to
express exclusiveor. This is one way to interpret the distributive law
of multiplication over addition in modulo 2 arithmetic.



Theorem  pm2.54 788 
Theorem *2.54 of [WhiteheadRussell] p.
107.



Theorem  dfor 789 
Define disjunction (logical 'or'). Definition of [Margaris] p. 49.



Theorem  orrd 790 
Deduce implication from disjunction.



Theorem  orri 791 
Infer implication from disjunction.



Theorem  pm2.25 792 
Theorem *2.25 of [WhiteheadRussell] p.
104.



Theorem  pm2.68 793 
Theorem *2.68 of [WhiteheadRussell] p.
108.



Theorem  dfor2 794 
Logical 'or' expressed in terms of implication only. Theorem *5.25 of
[WhiteheadRussell] p. 124. (The
proof was shortened by Wolf Lammen,
20Oct2012.)



Theorem  pm4.64 795 
Theorem *4.64 of [WhiteheadRussell] p.
120.



Theorem  imor 796 
Implication in terms of disjunction. Theorem *4.6 of [WhiteheadRussell]
p. 120.



Theorem  imori 797 
Infer disjunction from implication.



Theorem  exmid 798 
Law of excluded middle, also called the principle of tertium non datur.
Theorem *2.11 of [WhiteheadRussell] p. 101. It says that
something is
either true or not true; there are no inbetween values of truth. This is
an essential distinction of our classical logic and is not a theorem of
intuitionistic logic.



Theorem  pm2.1 799 
Theorem *2.1 of [WhiteheadRussell] p.
101. (The proof was shortened by
Wolf Lammen, 23Nov2012.)



Theorem  pm2.13 800 
Theorem *2.13 of [WhiteheadRussell] p.
101.

