P. 10 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 901-1000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bigolden 901	Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
⊢ (((φ ∧ ψ) ↔ φ) ↔ (ψ ↔ (φ ∨ ψ)))
Theorem	pm5.71 902	Theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.)
⊢ ((ψ → ¬ χ) → (((φ ∨ ψ) ∧ χ) ↔ (φ ∧ χ)))
Theorem	pm5.75 903	Theorem *5.75 of [WhiteheadRussell] p. 126. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2012.)
⊢ (((χ → ¬ ψ) ∧ (φ ↔ (ψ ∨ χ))) → ((φ ∧ ¬ ψ) ↔ χ))
Theorem	bimsc1 904	Removal of conjunct from one side of an equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (((φ → ψ) ∧ (χ ↔ (ψ ∧ φ))) → (χ ↔ φ))
Theorem	4exmid 905	The disjunction of the four possible combinations of two wffs and their negations is always true. (Contributed by David Abernethy, 28-Jan-2014.)
⊢ (((φ ∧ ψ) ∨ (¬ φ ∧ ¬ ψ)) ∨ ((φ ∧ ¬ ψ) ∨ (ψ ∧ ¬ φ)))
Theorem	ecase2d 906	Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Dec-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → ¬ (ψ ∧ χ))    &   ⊢ (φ → ¬ (ψ ∧ θ))    &   ⊢ (φ → (τ ∨ (χ ∨ θ)))    ⇒   ⊢ (φ → τ)
Theorem	ecase3 907	Inference for elimination by cases. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
⊢ (φ → χ)    &   ⊢ (ψ → χ)    &   ⊢ (¬ (φ ∨ ψ) → χ)    ⇒   ⊢ χ
Theorem	ecase 908	Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.)
⊢ (¬ φ → χ)    &   ⊢ (¬ ψ → χ)    &   ⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ χ
Theorem	ecase3d 909	Deduction for elimination by cases. (Contributed by NM, 2-May-1996.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (φ → (ψ → θ))    &   ⊢ (φ → (χ → θ))    &   ⊢ (φ → (¬ (ψ ∨ χ) → θ))    ⇒   ⊢ (φ → θ)
Theorem	ecased 910	Deduction for elimination by cases. (Contributed by NM, 8-Oct-2012.)
⊢ (φ → (¬ ψ → θ))    &   ⊢ (φ → (¬ χ → θ))    &   ⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ (φ → θ)
Theorem	ecase3ad 911	Deduction for elimination by cases. (Contributed by NM, 24-May-2013.)
⊢ (φ → (ψ → θ))    &   ⊢ (φ → (χ → θ))    &   ⊢ (φ → ((¬ ψ ∧ ¬ χ) → θ))    ⇒   ⊢ (φ → θ)
Theorem	ccase 912	Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
⊢ ((φ ∧ ψ) → τ)    &   ⊢ ((χ ∧ ψ) → τ)    &   ⊢ ((φ ∧ θ) → τ)    &   ⊢ ((χ ∧ θ) → τ)    ⇒   ⊢ (((φ ∨ χ) ∧ (ψ ∨ θ)) → τ)
Theorem	ccased 913	Deduction for combining cases. (Contributed by NM, 9-May-2004.)
⊢ (φ → ((ψ ∧ χ) → η))    &   ⊢ (φ → ((θ ∧ χ) → η))    &   ⊢ (φ → ((ψ ∧ τ) → η))    &   ⊢ (φ → ((θ ∧ τ) → η))    ⇒   ⊢ (φ → (((ψ ∨ θ) ∧ (χ ∨ τ)) → η))
Theorem	ccase2 914	Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
⊢ ((φ ∧ ψ) → τ)    &   ⊢ (χ → τ)    &   ⊢ (θ → τ)    ⇒   ⊢ (((φ ∨ χ) ∧ (ψ ∨ θ)) → τ)
Theorem	4cases 915	Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 25-Oct-2003.)
⊢ ((φ ∧ ψ) → χ)    &   ⊢ ((φ ∧ ¬ ψ) → χ)    &   ⊢ ((¬ φ ∧ ψ) → χ)    &   ⊢ ((¬ φ ∧ ¬ ψ) → χ)    ⇒   ⊢ χ
Theorem	4casesdan 916	Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 19-Mar-2013.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    &   ⊢ ((φ ∧ (ψ ∧ ¬ χ)) → θ)    &   ⊢ ((φ ∧ (¬ ψ ∧ χ)) → θ)    &   ⊢ ((φ ∧ (¬ ψ ∧ ¬ χ)) → θ)    ⇒   ⊢ (φ → θ)
Theorem	niabn 917	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
⊢ φ    ⇒   ⊢ (¬ ψ → ((χ ∧ ψ) ↔ ¬ φ))
Theorem	dedlem0a 918	Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (φ → (ψ ↔ ((χ → φ) → (ψ ∧ φ))))
Theorem	dedlem0b 919	Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.)
⊢ (¬ φ → (ψ ↔ ((ψ → φ) → (χ ∧ φ))))
Theorem	dedlema 920	Lemma for weak deduction theorem. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (φ → (ψ ↔ ((ψ ∧ φ) ∨ (χ ∧ ¬ φ))))
Theorem	dedlemb 921	Lemma for weak deduction theorem. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (¬ φ → (χ ↔ ((ψ ∧ φ) ∨ (χ ∧ ¬ φ))))
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, 26-Jun-2002.)
⊢ ((φ ↔ ((φ ∧ χ) ∨ (ψ ∧ ¬ χ))) → (χ ↔ τ))    &   ⊢ ((ψ ↔ ((φ ∧ χ) ∨ (ψ ∧ ¬ χ))) → (θ ↔ τ))    &   ⊢ θ    ⇒   ⊢ τ
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, 26-Jun-2002.)
⊢ ((φ ↔ ((φ ∧ χ) ∨ (ψ ∧ ¬ χ))) → (θ ↔ τ))    &   ⊢ τ    ⇒   ⊢ (χ → θ)
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, 27-Jun-2002.) (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 left-hand side is redundant. (Contributed by NM, 16-May-2003.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 20-Jan-2013.)
⊢ ((((φ ∧ ψ) ∨ (¬ φ ∧ χ)) ∨ (ψ ∧ χ)) ↔ ((φ ∧ ψ) ∨ (¬ φ ∧ χ)))
Theorem	pm4.42 926	Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed by Roy F. Longton, 21-Jun-2005.)
⊢ (φ ↔ ((φ ∧ ψ) ∨ (φ ∧ ¬ ψ)))
Theorem	ninba 927	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
⊢ φ    ⇒   ⊢ (¬ ψ → (¬ φ ↔ (χ ∧ ψ)))
Theorem	prlem1 928	A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
⊢ (φ → (η ↔ χ))    &   ⊢ (ψ → ¬ θ)    ⇒   ⊢ (φ → (ψ → (((ψ ∧ χ) ∨ (θ ∧ τ)) → η)))
Theorem	prlem2 929	A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
⊢ (((φ ∧ ψ) ∨ (χ ∧ θ)) ↔ ((φ ∨ χ) ∧ ((φ ∧ ψ) ∨ (χ ∧ θ))))
Theorem	oplem1 930	A specialized lemma for set theory (ordered pair theorem). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Wolf Lammen, 8-Dec-2012.)
⊢ (φ → (ψ ∨ χ))    &   ⊢ (φ → (θ ∨ τ))    &   ⊢ (ψ ↔ θ)    &   ⊢ (χ → (θ ↔ τ))    ⇒   ⊢ (φ → ψ)
Theorem	rnlem 931	Lemma used in construction of real numbers. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) ↔ (((φ ∧ χ) ∧ (ψ ∧ θ)) ∧ ((φ ∧ θ) ∧ (ψ ∧ χ))))
Theorem	dn1 932	A single axiom for Boolean algebra known as DN1. See http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf. (Contributed by Jeffrey Hankins, 3-Jul-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
⊢ (¬ (¬ (¬ (φ ∨ ψ) ∨ χ) ∨ ¬ (φ ∨ ¬ (¬ χ ∨ ¬ (χ ∨ θ)))) ↔ χ)
1.2.8  Abbreviated conjunction and disjunction of three wff's
Syntax	w3o 933	Extend wff definition to include 3-way disjunction ('or').
wff (φ ∨ ψ ∨ χ)
Syntax	w3a 934	Extend wff definition to include 3-way conjunction ('and').
wff (φ ∧ ψ ∧ χ)
Definition	df-3or 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, 8-Apr-1994.)
⊢ ((φ ∨ ψ ∨ χ) ↔ ((φ ∨ ψ) ∨ χ))
Definition	df-3an 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, 8-Apr-1994.)
⊢ ((φ ∧ ψ ∧ χ) ↔ ((φ ∧ ψ) ∧ χ))
Theorem	3orass 937	Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((φ ∨ ψ ∨ χ) ↔ (φ ∨ (ψ ∨ χ)))
Theorem	3anass 938	Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((φ ∧ ψ ∧ χ) ↔ (φ ∧ (ψ ∧ χ)))
Theorem	3anrot 939	Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((φ ∧ ψ ∧ χ) ↔ (ψ ∧ χ ∧ φ))
Theorem	3orrot 940	Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
⊢ ((φ ∨ ψ ∨ χ) ↔ (ψ ∨ χ ∨ φ))
Theorem	3ancoma 941	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((φ ∧ ψ ∧ χ) ↔ (ψ ∧ φ ∧ χ))
Theorem	3orcoma 942	Commutation law for triple disjunction. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ ((φ ∨ ψ ∨ χ) ↔ (ψ ∨ φ ∨ χ))
Theorem	3ancomb 943	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((φ ∧ ψ ∧ χ) ↔ (φ ∧ χ ∧ ψ))
Theorem	3orcomb 944	Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ ((φ ∨ ψ ∨ χ) ↔ (φ ∨ χ ∨ ψ))
Theorem	3anrev 945	Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((φ ∧ ψ ∧ χ) ↔ (χ ∧ ψ ∧ φ))
Theorem	3anan32 946	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ ((φ ∧ ψ ∧ χ) ↔ ((φ ∧ χ) ∧ ψ))
Theorem	3anan12 947	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ ((φ ∧ ψ ∧ χ) ↔ (ψ ∧ (φ ∧ χ)))
Theorem	3anor 948	Triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.)
⊢ ((φ ∧ ψ ∧ χ) ↔ ¬ (¬ φ ∨ ¬ ψ ∨ ¬ χ))
Theorem	3ianor 949	Negated triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ (¬ (φ ∧ ψ ∧ χ) ↔ (¬ φ ∨ ¬ ψ ∨ ¬ χ))
Theorem	3ioran 950	Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)
⊢ (¬ (φ ∨ ψ ∨ χ) ↔ (¬ φ ∧ ¬ ψ ∧ ¬ χ))
Theorem	3oran 951	Triple disjunction in terms of triple conjunction. (Contributed by NM, 8-Oct-2012.)
⊢ ((φ ∨ ψ ∨ χ) ↔ ¬ (¬ φ ∧ ¬ ψ ∧ ¬ χ))
Theorem	3simpa 952	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((φ ∧ ψ ∧ χ) → (φ ∧ ψ))
Theorem	3simpb 953	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((φ ∧ ψ ∧ χ) → (φ ∧ χ))
Theorem	3simpc 954	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ ((φ ∧ ψ ∧ χ) → (ψ ∧ χ))
Theorem	simp1 955	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((φ ∧ ψ ∧ χ) → φ)
Theorem	simp2 956	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((φ ∧ ψ ∧ χ) → ψ)
Theorem	simp3 957	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((φ ∧ ψ ∧ χ) → χ)
Theorem	simpl1 958	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ (((φ ∧ ψ ∧ χ) ∧ θ) → φ)
Theorem	simpl2 959	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ (((φ ∧ ψ ∧ χ) ∧ θ) → ψ)
Theorem	simpl3 960	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ (((φ ∧ ψ ∧ χ) ∧ θ) → χ)
Theorem	simpr1 961	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ ((φ ∧ (ψ ∧ χ ∧ θ)) → ψ)
Theorem	simpr2 962	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ ((φ ∧ (ψ ∧ χ ∧ θ)) → χ)
Theorem	simpr3 963	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ ((φ ∧ (ψ ∧ χ ∧ θ)) → θ)
Theorem	simp1i 964	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
⊢ (φ ∧ ψ ∧ χ)    ⇒   ⊢ φ
Theorem	simp2i 965	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
⊢ (φ ∧ ψ ∧ χ)    ⇒   ⊢ ψ
Theorem	simp3i 966	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
⊢ (φ ∧ ψ ∧ χ)    ⇒   ⊢ χ
Theorem	simp1d 967	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
⊢ (φ → (ψ ∧ χ ∧ θ))    ⇒   ⊢ (φ → ψ)
Theorem	simp2d 968	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
⊢ (φ → (ψ ∧ χ ∧ θ))    ⇒   ⊢ (φ → χ)
Theorem	simp3d 969	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
⊢ (φ → (ψ ∧ χ ∧ θ))    ⇒   ⊢ (φ → θ)
Theorem	simp1bi 970	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (φ ↔ (ψ ∧ χ ∧ θ))    ⇒   ⊢ (φ → ψ)
Theorem	simp2bi 971	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (φ ↔ (ψ ∧ χ ∧ θ))    ⇒   ⊢ (φ → χ)
Theorem	simp3bi 972	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (φ ↔ (ψ ∧ χ ∧ θ))    ⇒   ⊢ (φ → θ)
Theorem	3adant1 973	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ ((θ ∧ φ ∧ ψ) → χ)
Theorem	3adant2 974	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ ((φ ∧ θ ∧ ψ) → χ)
Theorem	3adant3 975	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ ((φ ∧ ψ ∧ θ) → χ)
Theorem	3ad2ant1 976	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
⊢ (φ → χ)    ⇒   ⊢ ((φ ∧ ψ ∧ θ) → χ)
Theorem	3ad2ant2 977	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
⊢ (φ → χ)    ⇒   ⊢ ((ψ ∧ φ ∧ θ) → χ)
Theorem	3ad2ant3 978	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
⊢ (φ → χ)    ⇒   ⊢ ((ψ ∧ θ ∧ φ) → χ)
Theorem	simp1l 979	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
⊢ (((φ ∧ ψ) ∧ χ ∧ θ) → φ)
Theorem	simp1r 980	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
⊢ (((φ ∧ ψ) ∧ χ ∧ θ) → ψ)
Theorem	simp2l 981	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
⊢ ((φ ∧ (ψ ∧ χ) ∧ θ) → ψ)
Theorem	simp2r 982	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
⊢ ((φ ∧ (ψ ∧ χ) ∧ θ) → χ)
Theorem	simp3l 983	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
⊢ ((φ ∧ ψ ∧ (χ ∧ θ)) → χ)
Theorem	simp3r 984	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
⊢ ((φ ∧ ψ ∧ (χ ∧ θ)) → θ)
Theorem	simp11 985	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ (((φ ∧ ψ ∧ χ) ∧ θ ∧ τ) → φ)
Theorem	simp12 986	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ (((φ ∧ ψ ∧ χ) ∧ θ ∧ τ) → ψ)
Theorem	simp13 987	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ (((φ ∧ ψ ∧ χ) ∧ θ ∧ τ) → χ)
Theorem	simp21 988	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ ((φ ∧ (ψ ∧ χ ∧ θ) ∧ τ) → ψ)
Theorem	simp22 989	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ ((φ ∧ (ψ ∧ χ ∧ θ) ∧ τ) → χ)
Theorem	simp23 990	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ ((φ ∧ (ψ ∧ χ ∧ θ) ∧ τ) → θ)
Theorem	simp31 991	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ ((φ ∧ ψ ∧ (χ ∧ θ ∧ τ)) → χ)
Theorem	simp32 992	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ ((φ ∧ ψ ∧ (χ ∧ θ ∧ τ)) → θ)
Theorem	simp33 993	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ ((φ ∧ ψ ∧ (χ ∧ θ ∧ τ)) → τ)
Theorem	simpll1 994	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ ∧ χ) ∧ θ) ∧ τ) → φ)
Theorem	simpll2 995	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ ∧ χ) ∧ θ) ∧ τ) → ψ)
Theorem	simpll3 996	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ ∧ χ) ∧ θ) ∧ τ) → χ)
Theorem	simplr1 997	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ (φ ∧ ψ ∧ χ)) ∧ τ) → φ)
Theorem	simplr2 998	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ (φ ∧ ψ ∧ χ)) ∧ τ) → ψ)
Theorem	simplr3 999	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ (φ ∧ ψ ∧ χ)) ∧ τ) → χ)
Theorem	simprl1 1000	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ ((φ ∧ ψ ∧ χ) ∧ θ)) → φ)