P. 10 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 901-1000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pm4.43 901	Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ ¬ 𝜓)))
Theorem	pm4.82 902	Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ↔ ¬ 𝜑)
Theorem	pm4.83dc 903	Theorem *4.83 of [WhiteheadRussell] p. 122, for decidable propositions. As with other case elimination theorems, like pm2.61dc 806, it only holds for decidable propositions. (Contributed by Jim Kingdon, 12-May-2018.)
⊢ (DECID 𝜑 → (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜓)) ↔ 𝜓))
Theorem	biantr 904	A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 18-Aug-1993.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜓)) → (𝜑 ↔ 𝜒))
Theorem	orbididc 905	Disjunction distributes over the biconditional, for a decidable proposition. Based on 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. (Contributed by Jim Kingdon, 2-Apr-2018.)
⊢ (DECID 𝜑 → ((𝜑 ∨ (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ 𝜒))))
Theorem	pm5.7dc 906	Disjunction distributes over the biconditional, for a decidable proposition. Based on theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbididc 905. (Contributed by Jim Kingdon, 2-Apr-2018.)
⊢ (DECID 𝜒 → (((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) ↔ (𝜒 ∨ (𝜑 ↔ 𝜓))))
Theorem	bigolden 907	Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓)))
Theorem	anordc 908	Conjunction in terms of disjunction (DeMorgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120, but where the propositions are decidable. The forward direction, pm3.1 712, holds for all propositions, but the equivalence only holds given decidability. (Contributed by Jim Kingdon, 21-Apr-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ 𝜓) ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓))))
Theorem	pm3.11dc 909	Theorem *3.11 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, pm3.1 712, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 22-Apr-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (¬ 𝜑 ∨ ¬ 𝜓) → (𝜑 ∧ 𝜓))))
Theorem	pm3.12dc 910	Theorem *3.12 of [WhiteheadRussell] p. 111, but for decidable propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓))))
Theorem	pm3.13dc 911	Theorem *3.13 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, pm3.14 711, holds for all propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓))))
Theorem	dn1dc 912	DN1 for decidable propositions. Without the decidability conditions, DN1 can serve as a single axiom for Boolean algebra. See http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf. (Contributed by Jim Kingdon, 22-Apr-2018.)
⊢ ((DECID 𝜑 ∧ (DECID 𝜓 ∧ (DECID 𝜒 ∧ DECID 𝜃))) → (¬ (¬ (¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))) ↔ 𝜒))
Theorem	pm5.71dc 913	Decidable proposition version of theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.) (Modified for decidability by Jim Kingdon, 19-Apr-2018.)
⊢ (DECID 𝜓 → ((𝜓 → ¬ 𝜒) → (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ 𝜒))))
Theorem	pm5.75 914	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 915	Removal of conjunct from one side of an equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 ↔ (𝜓 ∧ 𝜑))) → (𝜒 ↔ 𝜑))
Theorem	ccase 916	Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
⊢ ((𝜑 ∧ 𝜓) → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜓) → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏)
Theorem	ccased 917	Deduction for combining cases. (Contributed by NM, 9-May-2004.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜂))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂))    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → 𝜂))
Theorem	ccase2 918	Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
⊢ ((𝜑 ∧ 𝜓) → 𝜏)    &   ⊢ (𝜒 → 𝜏)    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏)
Theorem	niabn 919	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜓 → ((𝜒 ∧ 𝜓) ↔ ¬ 𝜑))
Theorem	dedlem0a 920	Alternate version of dedlema 921. (Contributed by NM, 2-Apr-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (𝜑 → (𝜓 ↔ ((𝜒 → 𝜑) → (𝜓 ∧ 𝜑))))
Theorem	dedlema 921	Lemma for iftrue 3426. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → (𝜓 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑))))
Theorem	dedlemb 922	Lemma for iffalse 3429. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (¬ 𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑))))
Theorem	pm4.42r 923	One direction of Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed by Jim Kingdon, 4-Aug-2018.)
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓)) → 𝜑)
Theorem	ninba 924	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜓 → (¬ 𝜑 ↔ (𝜒 ∧ 𝜓)))
Theorem	prlem1 925	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 926	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 927	A specialized lemma for set theory (ordered pair theorem). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Wolf Lammen, 8-Dec-2012.) (Proof shortened by Mario Carneiro, 2-Feb-2015.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    &   ⊢ (𝜑 → (𝜃 ∨ 𝜏))    &   ⊢ (𝜓 ↔ 𝜃)    &   ⊢ (𝜒 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	rnlem 928	Lemma used in construction of real numbers. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜒))))
1.2.12  Abbreviated conjunction and disjunction of three wff's
Syntax	w3o 929	Extend wff definition to include 3-way disjunction ('or').
wff (𝜑 ∨ 𝜓 ∨ 𝜒)
Syntax	w3a 930	Extend wff definition to include 3-way conjunction ('and').
wff (𝜑 ∧ 𝜓 ∧ 𝜒)
Definition	df-3or 931	Define disjunction ('or') of 3 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 725. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
Definition	df-3an 932	Define conjunction ('and') of 3 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 396. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
Theorem	3orass 933	Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
Theorem	3anass 934	Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
Theorem	3anrot 935	Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
Theorem	3orrot 936	Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))
Theorem	3ancoma 937	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
Theorem	3ancomb 938	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))
Theorem	3orcomb 939	Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓))
Theorem	3anrev 940	Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓 ∧ 𝜑))
Theorem	3anan32 941	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
Theorem	3anan12 942	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
Theorem	anandi3 943	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
Theorem	anandi3r 944	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜓)))
Theorem	3ioran 945	Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)
⊢ (¬ (𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒))
Theorem	3simpa 946	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))
Theorem	3simpb 947	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒))
Theorem	3simpc 948	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
Theorem	simp1 949	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
Theorem	simp2 950	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
Theorem	simp3 951	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
Theorem	simpl1 952	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)
Theorem	simpl2 953	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)
Theorem	simpl3 954	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)
Theorem	simpr1 955	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓)
Theorem	simpr2 956	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒)
Theorem	simpr3 957	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃)
Theorem	simp1i 958	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)    ⇒   ⊢ 𝜑
Theorem	simp2i 959	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)    ⇒   ⊢ 𝜓
Theorem	simp3i 960	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)    ⇒   ⊢ 𝜒
Theorem	simp1d 961	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	simp2d 962	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	simp3d 963	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	simp1bi 964	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	simp2bi 965	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	simp3bi 966	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	3adant1 967	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)
Theorem	3adant2 968	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒)
Theorem	3adant3 969	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)
Theorem	3ad2ant1 970	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)
Theorem	3ad2ant2 971	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒)
Theorem	3ad2ant3 972	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)
Theorem	simp1l 973	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
Theorem	simp1r 974	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)
Theorem	simp2l 975	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)
Theorem	simp2r 976	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)
Theorem	simp3l 977	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)
Theorem	simp3r 978	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)
Theorem	simp11 979	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑)
Theorem	simp12 980	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓)
Theorem	simp13 981	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒)
Theorem	simp21 982	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓)
Theorem	simp22 983	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜒)
Theorem	simp23 984	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜃)
Theorem	simp31 985	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜒)
Theorem	simp32 986	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃)
Theorem	simp33 987	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏)
Theorem	simpll1 988	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Theorem	simpll2 989	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Theorem	simpll3 990	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)
Theorem	simplr1 991	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑)
Theorem	simplr2 992	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓)
Theorem	simplr3 993	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒)
Theorem	simprl1 994	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑)
Theorem	simprl2 995	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)
Theorem	simprl3 996	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)
Theorem	simprr1 997	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑)
Theorem	simprr2 998	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓)
Theorem	simprr3 999	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒)
Theorem	simpl1l 1000	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑)