Type  Label  Description 
Statement 

Theorem  pm4.62 801 
Theorem *4.62 of [WhiteheadRussell] p.
120.



Theorem  pm4.66 802 
Theorem *4.66 of [WhiteheadRussell] p.
120.



Theorem  ianor 803 
Negated conjunction in terms of disjunction (DeMorgan's law). Theorem
*4.51 of [WhiteheadRussell] p.
120. (The proof was shortened by Andrew
Salmon, 13May2011.)



Theorem  anor 804 
Conjunction in terms of disjunction (DeMorgan's law). Theorem *4.5 of
[WhiteheadRussell] p. 120. (The
proof was shortened by Wolf Lammen,
3Nov2012.)



Theorem  ioranOLD 805 
Obsolete proof of ioran 645 as of 28Sep2014.



Theorem  oibabs 806 
Absorption of disjunction into equivalence. (The proof was shortened by
Wolf Lammen, 3Nov2013.)



Theorem  pm4.52 807 
Theorem *4.52 of [WhiteheadRussell] p.
120. (The proof was shortened by
Wolf Lammen, 5Nov2012.)



Theorem  pm4.53 808 
Theorem *4.53 of [WhiteheadRussell] p.
120.



Theorem  pm4.54 809 
Theorem *4.54 of [WhiteheadRussell] p.
120. (The proof was shortened by
Wolf Lammen, 5Nov2012.)



Theorem  pm4.54OLD 810 
Obsolete proof of pm4.54 809 as of 28Sep2014.



Theorem  pm4.55 811 
Theorem *4.55 of [WhiteheadRussell] p.
120.



Theorem  pm4.56 812 
Theorem *4.56 of [WhiteheadRussell] p.
120.



Theorem  oran 813 
Disjunction in terms of conjunction (DeMorgan's law). Compare Theorem
*4.57 of [WhiteheadRussell] p.
120. (The proof was shortened by Andrew
Salmon, 7May2011.)



Theorem  pm4.57 814 
Theorem *4.57 of [WhiteheadRussell] p.
120.



Theorem  pm3.11 815 
Theorem *3.11 of [WhiteheadRussell] p.
111.



Theorem  pm3.12 816 
Theorem *3.12 of [WhiteheadRussell] p.
111.



Theorem  pm3.13 817 
Theorem *3.13 of [WhiteheadRussell] p.
111.



Theorem  pm4.78 818 
Theorem *4.78 of [WhiteheadRussell] p.
121. (The proof was shortened by
Wolf Lammen, 19Nov2012.)



Theorem  pm4.79 819 
Theorem *4.79 of [WhiteheadRussell] p.
121. (The proof was shortened by
Wolf Lammen, 27Jun2013.)



Theorem  pm5.17 820 
Theorem *5.17 of [WhiteheadRussell] p.
124. (The proof was shortened by
Wolf Lammen, 3Jan2013.)



Theorem  orimdi 821 
Disjunction distributes over implication. (Contributed by Wolf Lammen,
5Jan2013.)



Theorem  pm2.85 822 
Theorem *2.85 of [WhiteheadRussell] p.
108. (The proof was shortened by
Wolf Lammen, 5Jan2013.)



Theorem  xor 823 
Two ways to express "exclusive or." Theorem *5.22 of [WhiteheadRussell]
p. 124. (The proof was shortened by Wolf Lammen, 22Jan2013.)



Theorem  xor2 824 
Two ways to express "exclusive or." (The proof was shortened by Wolf
Lammen, 24Jan2013.)



Theorem  dfbi3 825 
An alternate definition of the biconditional. Theorem *5.23 of
[WhiteheadRussell] p. 124. (The
proof was shortened by Wolf Lammen,
3Nov2013.)



Theorem  pm5.24 826 
Theorem *5.24 of [WhiteheadRussell] p.
124.



Theorem  jcabOLD 827 
Obsolete proof of jcab 517 as of 27Nov2013



Theorem  imimorb 828 
Simplify an implication between implications. (Contributed by Paul
Chapman, 17Nov2012.) (The proof was shortened by Wolf Lammen,
3Apr2013.)



Theorem  pm2.26 829 
Theorem *2.26 of [WhiteheadRussell] p.
104. (The proof was shortened by
Wolf Lammen, 23Nov2012.)



Theorem  pm5.11 830 
Theorem *5.11 of [WhiteheadRussell] p.
123.



Theorem  pm5.12 831 
Theorem *5.12 of [WhiteheadRussell] p.
123.



Theorem  pm5.14 832 
Theorem *5.14 of [WhiteheadRussell] p.
123.



Theorem  pm5.13 833 
Theorem *5.13 of [WhiteheadRussell] p.
123. (The proof was shortened by
Wolf Lammen, 14Nov2012.)



Theorem  pm5.15 834 
Theorem *5.15 of [WhiteheadRussell] p.
124. (The proof was shortened by
Wolf Lammen, 15Oct2013.)



Theorem  pm5.55 835 
Theorem *5.55 of [WhiteheadRussell] p.
125. (The proof was shortened by
Wolf Lammen, 20Jan2013.)



1.2.8 Miscellaneous theorems of propositional
calculus


Theorem  pm5.21nd 836 
Eliminate an antecedent implied by each side of a biconditional. (The
proof was shortened by Wolf Lammen, 4Nov2013.)



Theorem  pm5.35 837 
Theorem *5.35 of [WhiteheadRussell] p.
125.



Theorem  pm5.54 838 
Theorem *5.54 of [WhiteheadRussell] p.
125. (The proof was shortened by
Wolf Lammen, 7Nov2013.)



Theorem  baib 839 
Move conjunction outside of biconditional.



Theorem  baibr 840 
Move conjunction outside of biconditional.



Theorem  pm5.44 841 
Theorem *5.44 of [WhiteheadRussell] p.
125.



Theorem  pm5.6 842 
Conjunction in antecedent versus disjunction in consequent. Theorem *5.6
of [WhiteheadRussell] p. 125.



Theorem  orcanai 843 
Change disjunction in consequent to conjunction in antecedent.



Theorem  intnan 844 
Introduction of conjunct inside of a contradiction.



Theorem  intnanr 845 
Introduction of conjunct inside of a contradiction.



Theorem  intnand 846 
Introduction of conjunct inside of a contradiction.



Theorem  intnanrd 847 
Introduction of conjunct inside of a contradiction.



Theorem  mpbiran 848 
Detach truth from conjunction in biconditional.



Theorem  mpbiran2 849 
Detach truth from conjunction in biconditional.



Theorem  mpbir2an 850 
Detach a conjunction of truths in a biconditional.



Theorem  mpbi2and 851 
Detach a conjunction of truths in a biconditional. (The proof was
shortened by Wolf Lammen, 24Nov2012.)



Theorem  mpbir2and 852 
Detach a conjunction of truths in a biconditional. (The proof was
shortened by Wolf Lammen, 24Nov2012.)



Theorem  mpbiranOLD 853 
Obsolete version of mpbiran 848 as of 9Jan2015.



Theorem  mpbiran2OLD 854 
Obsolete version of mpbiran2 849 as of 9Jan2015.



Theorem  mpbir2anOLD 855 
Obsolete version of mpbir2an 850 as of 9Jan2015.



Theorem  mpbi2andOLD 856 
Obsolete version of mpbi2and 851 as of 9Jan2015.



Theorem  mpbir2andOLD 857 
Obsolete version of mpbir2and 852 as of 9Jan2015.



Theorem  pm5.62 858 
Theorem *5.62 of [WhiteheadRussell] p.
125. (Contributed by Roy F.
Longton, 21Jun2005.)



Theorem  pm5.63 859 
Theorem *5.63 of [WhiteheadRussell] p.
125. (The proof was shortened by
Wolf Lammen, 25Dec2012.)



Theorem  bianfi 860 
A wff conjoined with falsehood is false. (The proof was shortened by
Wolf Lammen, 26Nov2012.)



Theorem  bianfd 861 
A wff conjoined with falsehood is false. (The proof was shortened by
Wolf Lammen, 5Nov2013.)



Theorem  pm4.43 862 
Theorem *4.43 of [WhiteheadRussell] p.
119. (The proof was shortened by
Wolf Lammen, 26Nov2012.)



Theorem  pm4.82 863 
Theorem *4.82 of [WhiteheadRussell] p.
122.



Theorem  pm4.83 864 
Theorem *4.83 of [WhiteheadRussell] p.
122.



Theorem  pclem6 865 
Negation inferred from embedded conjunct. (The proof was shortened by
Wolf Lammen, 25Nov2012.)



Theorem  biantr 866 
A transitive law of equivalence. Compare Theorem *4.22 of
[WhiteheadRussell] p. 117.



Theorem  orbidi 867 
Disjunction distributes over the biconditional. An axiom of system DS in
Vladimir Lifschitz, "On calculational proofs" (1998),
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.3384.
(The
proof was shortened by Wolf Lammen, 4Feb2013.)



Theorem  biluk 868 
Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall,
ed., Polish Logic 19201939 (Oxford, 1967), p. 96.



Theorem  pm5.7 869 
Disjunction distributes over the biconditional. Theorem *5.7 of
[WhiteheadRussell] p. 125. This
theorem is similar to orbidi 867.
(Contributed by Roy F. Longton, 21Jun2005.)



Theorem  bigolden 870 
DijkstraScholten's Golden Rule for calculational proofs.



Theorem  pm5.71 871 
Theorem *5.71 of [WhiteheadRussell] p.
125. (Contributed by Roy F.
Longton, 23Jun2005.)



Theorem  pm5.75 872 
Theorem *5.75 of [WhiteheadRussell] p.
126. (The proof was shortened by
Andrew Salmon, 7May2011.) (The proof was shortened by Wolf Lammen,
23Dec2012.)



Theorem  bimsc1 873 
Removal of conjunct from one side of an equivalence.



Theorem  4exmid 874 
The disjunction of the four possible combinations of two wffs and their
negations is always true. (Contributed by David Abernethy,
28Jan2014.)



Theorem  ecase2d 875 
Deduction for elimination by cases. (The proof was shortened by Wolf
Lammen, 22Dec2012.)



Theorem  ecase3 876 
Inference for elimination by cases. (The proof was shortened by Wolf
Lammen, 26Nov2012.)



Theorem  ecase 877 
Inference for elimination by cases.



Theorem  ecase3d 878 
Deduction for elimination by cases. (The proof was shortened by Andrew
Salmon, 7May2011.)



Theorem  ecased 879 
Deduction for elimination by cases.



Theorem  ecase3ad 880 
Deduction for elimination by cases.



Theorem  ccase 881 
Inference for combining cases. (The proof was shortened by Wolf Lammen,
6Jan2013.)



Theorem  ccased 882 
Deduction for combining cases.



Theorem  ccase2 883 
Inference for combining cases.



Theorem  4cases 884 
Inference eliminating two antecedents from the four possible cases that
result from their true/false combinations.



Theorem  4casesdan 885 
Deduction eliminating two antecedents from the four possible cases that
result from their true/false combinations.



Theorem  niabn 886 
Miscellaneous inference relating falsehoods.



Theorem  dedlem0a 887 
Lemma for an alternate version of weak deduction theorem. (The proof was
shortened by Andrew Salmon, 7May2011.) (The proof was shortened by Wolf
Lammen, 4Dec2012.)



Theorem  dedlem0b 888 
Lemma for an alternate version of weak deduction theorem.



Theorem  dedlema 889 
Lemma for weak deduction theorem. (The proof was shortened by Andrew
Salmon, 7May2011.)



Theorem  dedlemb 890 
Lemma for weak deduction theorem. (The proof was shortened by Andrew
Salmon, 7May2011.)



Theorem  elimh 891 
Hypothesis builder for weak deduction theorem. For more information,
see the Deduction Theorem link on the Metamath Proof Explorer home
page.



Theorem  dedt 892 
The weak deduction theorem. For more information, see the Deduction
Theorem link on the Metamath Proof Explorer home page.



Theorem  con3th 893 
Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. This version
of con3 550 demonstrates the use of the weak deduction
theorem to derive it
from con3i 543.



Theorem  consensus 894 
The consensus theorem. This theorem and its dual (with and
interchanged) are commonly used in computer logic design to eliminate
redundant terms from Boolean expressions. Specifically, we prove that the
term
on the lefthand side is redundant. (The proof was
shortened by Andrew Salmon, 13May2011.) (The proof was shortened by
Wolf Lammen, 20Jan2013.)



Theorem  pm4.42 895 
Theorem *4.42 of [WhiteheadRussell] p.
119. (Contributed by Roy F.
Longton, 21Jun2005.)



Theorem  ninba 896 
Miscellaneous inference relating falsehoods.



Theorem  prlem1 897 
A specialized lemma for set theory (to derive the Axiom of Pairing).
(The proof was shortened by Andrew Salmon, 13May2011.) (The proof was
shortened by Wolf Lammen, 5Jan2013.)



Theorem  prlem2 898 
A specialized lemma for set theory (to derive the Axiom of Pairing). (The
proof was shortened by Andrew Salmon, 13May2011.) (The proof was
shortened by Wolf Lammen, 9Dec2012.)



Theorem  oplem1 899 
A specialized lemma for set theory (ordered pair theorem). (The proof
was shortened by Wolf Lammen, 8Dec2012.)
(The proof was shortened by Mario Carneiro, 2Feb2015.)



Theorem  rnlem 900 
Lemma used in construction of real numbers. (The proof was shortened by
Andrew Salmon, 26Jun2011.)

