Type  Label  Description 
Statement 

Theorem  bigolden 901 
DijkstraScholten's Golden Rule for calculational proofs. (Contributed by
NM, 10Jan2005.)



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



Theorem  pm5.75 903 
Theorem *5.75 of [WhiteheadRussell] p.
126. (Contributed by NM,
3Jan2005.) (Proof shortened by Andrew Salmon, 7May2011.) (Proof
shortened by Wolf Lammen, 23Dec2012.)



Theorem  bimsc1 904 
Removal of conjunct from one side of an equivalence. (Contributed by NM,
5Aug1993.)



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



Theorem  ecase2d 906 
Deduction for elimination by cases. (Contributed by NM, 21Apr1994.)
(Proof shortened by Wolf Lammen, 22Dec2012.)



Theorem  ecase3 907 
Inference for elimination by cases. (Contributed by NM, 23Mar1995.)
(Proof shortened by Wolf Lammen, 26Nov2012.)



Theorem  ecase 908 
Inference for elimination by cases. (Contributed by NM,
13Jul2005.)



Theorem  ecase3d 909 
Deduction for elimination by cases. (Contributed by NM, 2May1996.)
(Proof shortened by Andrew Salmon, 7May2011.)



Theorem  ecased 910 
Deduction for elimination by cases. (Contributed by NM, 8Oct2012.)



Theorem  ecase3ad 911 
Deduction for elimination by cases. (Contributed by NM,
24May2013.)



Theorem  ccase 912 
Inference for combining cases. (Contributed by NM, 29Jul1999.)
(Proof shortened by Wolf Lammen, 6Jan2013.)



Theorem  ccased 913 
Deduction for combining cases. (Contributed by NM, 9May2004.)



Theorem  ccase2 914 
Inference for combining cases. (Contributed by NM, 29Jul1999.)



Theorem  4cases 915 
Inference eliminating two antecedents from the four possible cases that
result from their true/false combinations. (Contributed by NM,
25Oct2003.)



Theorem  4casesdan 916 
Deduction eliminating two antecedents from the four possible cases that
result from their true/false combinations. (Contributed by NM,
19Mar2013.)



Theorem  niabn 917 
Miscellaneous inference relating falsehoods. (Contributed by NM,
31Mar1994.)



Theorem  dedlem0a 918 
Lemma for an alternate version of weak deduction theorem. (Contributed by
NM, 2Apr1994.) (Proof shortened by Andrew Salmon, 7May2011.) (Proof
shortened by Wolf Lammen, 4Dec2012.)



Theorem  dedlem0b 919 
Lemma for an alternate version of weak deduction theorem. (Contributed by
NM, 2Apr1994.)



Theorem  dedlema 920 
Lemma for weak deduction theorem. (Contributed by NM, 26Jun2002.)
(Proof shortened by Andrew Salmon, 7May2011.)



Theorem  dedlemb 921 
Lemma for weak deduction theorem. (Contributed by NM, 15May1999.)
(Proof shortened by Andrew Salmon, 7May2011.)



Theorem  elimh 922 
Hypothesis builder for weak deduction theorem. For more information,
see the Deduction Theorem link on the Metamath Proof Explorer home
page. (Contributed by NM, 26Jun2002.)



Theorem  dedt 923 
The weak deduction theorem. For more information, see the Deduction
Theorem link on the Metamath Proof Explorer home page. (Contributed by
NM, 26Jun2002.)



Theorem  con3th 924 
Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. This version
of con3 126 demonstrates the use of the weak deduction
theorem dedt 923 to
derive it from con3i 127. (Contributed by NM, 27Jun2002.)
(Proof modification is discouraged.)



Theorem  consensus 925 
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. (Contributed by
NM, 16May2003.) (Proof shortened by Andrew Salmon, 13May2011.)
(Proof shortened by Wolf Lammen, 20Jan2013.)



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



Theorem  ninba 927 
Miscellaneous inference relating falsehoods. (Contributed by NM,
31Mar1994.)



Theorem  prlem1 928 
A specialized lemma for set theory (to derive the Axiom of Pairing).
(Contributed by NM, 18Oct1995.) (Proof shortened by Andrew Salmon,
13May2011.) (Proof shortened by Wolf Lammen, 5Jan2013.)



Theorem  prlem2 929 
A specialized lemma for set theory (to derive the Axiom of Pairing).
(Contributed by NM, 5Aug1993.) (Proof shortened by Andrew Salmon,
13May2011.) (Proof shortened by Wolf Lammen, 9Dec2012.)



Theorem  oplem1 930 
A specialized lemma for set theory (ordered pair theorem). (Contributed
by NM, 18Oct1995.) (Proof shortened by Wolf Lammen, 8Dec2012.)



Theorem  rnlem 931 
Lemma used in construction of real numbers. (Contributed by NM,
4Sep1995.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  dn1 932 
A single axiom for Boolean algebra known as DN_{1}. See
http://wwwunix.mcs.anl.gov/~mccune/papers/basax/v12.pdf.
(Contributed by Jeffrey Hankins, 3Jul2009.) (Proof shortened by Andrew
Salmon, 13May2011.) (Proof shortened by Wolf Lammen, 6Jan2013.)



1.2.8 Abbreviated conjunction and disjunction of
three wff's


Syntax  w3o 933 
Extend wff definition to include 3way disjunction ('or').



Syntax  w3a 934 
Extend wff definition to include 3way conjunction ('and').



Definition  df3or 935 
Define disjunction ('or') of three wff's. Definition *2.33 of
[WhiteheadRussell] p. 105. This
abbreviation reduces the number of
parentheses and emphasizes that the order of bracketing is not important
by virtue of the associative law orass 510. (Contributed by NM,
8Apr1994.)



Definition  df3an 936 
Define conjunction ('and') of three wff's. Definition *4.34 of
[WhiteheadRussell] p. 118. This
abbreviation reduces the number of
parentheses and emphasizes that the order of bracketing is not important
by virtue of the associative law anass 630. (Contributed by NM,
8Apr1994.)



Theorem  3orass 937 
Associative law for triple disjunction. (Contributed by NM,
8Apr1994.)



Theorem  3anass 938 
Associative law for triple conjunction. (Contributed by NM,
8Apr1994.)



Theorem  3anrot 939 
Rotation law for triple conjunction. (Contributed by NM, 8Apr1994.)



Theorem  3orrot 940 
Rotation law for triple disjunction. (Contributed by NM, 4Apr1995.)



Theorem  3ancoma 941 
Commutation law for triple conjunction. (Contributed by NM,
21Apr1994.)



Theorem  3orcoma 942 
Commutation law for triple disjunction. (Contributed by Mario Carneiro,
4Sep2016.)



Theorem  3ancomb 943 
Commutation law for triple conjunction. (Contributed by NM,
21Apr1994.)



Theorem  3orcomb 944 
Commutation law for triple disjunction. (Contributed by Scott Fenton,
20Apr2011.)



Theorem  3anrev 945 
Reversal law for triple conjunction. (Contributed by NM, 21Apr1994.)



Theorem  3anan32 946 
Convert triple conjunction to conjunction, then commute. (Contributed by
Jonathan BenNaim, 3Jun2011.)



Theorem  3anan12 947 
Convert triple conjunction to conjunction, then commute. (Contributed by
Jonathan BenNaim, 3Jun2011.) (Proof shortened by Andrew Salmon,
14Jun2011.)



Theorem  3anor 948 
Triple conjunction expressed in terms of triple disjunction. (Contributed
by Jeff Hankins, 15Aug2009.)



Theorem  3ianor 949 
Negated triple conjunction expressed in terms of triple disjunction.
(Contributed by Jeff Hankins, 15Aug2009.) (Proof shortened by Andrew
Salmon, 13May2011.)



Theorem  3ioran 950 
Negated triple disjunction as triple conjunction. (Contributed by Scott
Fenton, 19Apr2011.)



Theorem  3oran 951 
Triple disjunction in terms of triple conjunction. (Contributed by NM,
8Oct2012.)



Theorem  3simpa 952 
Simplification of triple conjunction. (Contributed by NM,
21Apr1994.)



Theorem  3simpb 953 
Simplification of triple conjunction. (Contributed by NM,
21Apr1994.)



Theorem  3simpc 954 
Simplification of triple conjunction. (Contributed by NM, 21Apr1994.)
(Proof shortened by Andrew Salmon, 13May2011.)



Theorem  simp1 955 
Simplification of triple conjunction. (Contributed by NM,
21Apr1994.)



Theorem  simp2 956 
Simplification of triple conjunction. (Contributed by NM,
21Apr1994.)



Theorem  simp3 957 
Simplification of triple conjunction. (Contributed by NM,
21Apr1994.)



Theorem  simpl1 958 
Simplification rule. (Contributed by Jeff Hankins, 17Nov2009.)



Theorem  simpl2 959 
Simplification rule. (Contributed by Jeff Hankins, 17Nov2009.)



Theorem  simpl3 960 
Simplification rule. (Contributed by Jeff Hankins, 17Nov2009.)



Theorem  simpr1 961 
Simplification rule. (Contributed by Jeff Hankins, 17Nov2009.)



Theorem  simpr2 962 
Simplification rule. (Contributed by Jeff Hankins, 17Nov2009.)



Theorem  simpr3 963 
Simplification rule. (Contributed by Jeff Hankins, 17Nov2009.)



Theorem  simp1i 964 
Infer a conjunct from a triple conjunction. (Contributed by NM,
19Apr2005.)



Theorem  simp2i 965 
Infer a conjunct from a triple conjunction. (Contributed by NM,
19Apr2005.)



Theorem  simp3i 966 
Infer a conjunct from a triple conjunction. (Contributed by NM,
19Apr2005.)



Theorem  simp1d 967 
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4Sep2005.)



Theorem  simp2d 968 
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4Sep2005.)



Theorem  simp3d 969 
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4Sep2005.)



Theorem  simp1bi 970 
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
BenNaim, 3Jun2011.)



Theorem  simp2bi 971 
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
BenNaim, 3Jun2011.)



Theorem  simp3bi 972 
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
BenNaim, 3Jun2011.)



Theorem  3adant1 973 
Deduction adding a conjunct to antecedent. (Contributed by NM,
16Jul1995.)



Theorem  3adant2 974 
Deduction adding a conjunct to antecedent. (Contributed by NM,
16Jul1995.)



Theorem  3adant3 975 
Deduction adding a conjunct to antecedent. (Contributed by NM,
16Jul1995.)



Theorem  3ad2ant1 976 
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21Apr2005.)



Theorem  3ad2ant2 977 
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21Apr2005.)



Theorem  3ad2ant3 978 
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21Apr2005.)



Theorem  simp1l 979 
Simplification of triple conjunction. (Contributed by NM, 9Nov2011.)



Theorem  simp1r 980 
Simplification of triple conjunction. (Contributed by NM, 9Nov2011.)



Theorem  simp2l 981 
Simplification of triple conjunction. (Contributed by NM, 9Nov2011.)



Theorem  simp2r 982 
Simplification of triple conjunction. (Contributed by NM, 9Nov2011.)



Theorem  simp3l 983 
Simplification of triple conjunction. (Contributed by NM, 9Nov2011.)



Theorem  simp3r 984 
Simplification of triple conjunction. (Contributed by NM, 9Nov2011.)



Theorem  simp11 985 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp12 986 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp13 987 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp21 988 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp22 989 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp23 990 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp31 991 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp32 992 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp33 993 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simpll1 994 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpll2 995 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpll3 996 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simplr1 997 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simplr2 998 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simplr3 999 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simprl1 1000 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)

