P. 9 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 801-900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pm4.64dc 801	Theorem *4.64 of [WhiteheadRussell] p. 120, given a decidability condition. The reverse direction, pm2.53 641, holds for all propositions. (Contributed by Jim Kingdon, 2-May-2018.)
⊢ (DECID 𝜑 → ((¬ 𝜑 → 𝜓) ↔ (𝜑 ∨ 𝜓)))
Theorem	pm4.66dc 802	Theorem *4.66 of [WhiteheadRussell] p. 120, given a decidability condition. (Contributed by Jim Kingdon, 2-May-2018.)
⊢ (DECID 𝜑 → ((¬ 𝜑 → ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓)))
Theorem	pm4.52im 803	One direction of theorem *4.52 of [WhiteheadRussell] p. 120. The converse also holds in classical logic. (Contributed by Jim Kingdon, 27-Jul-2018.)
⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ (¬ 𝜑 ∨ 𝜓))
Theorem	pm4.53r 804	One direction of theorem *4.53 of [WhiteheadRussell] p. 120. The converse also holds in classical logic. (Contributed by Jim Kingdon, 27-Jul-2018.)
⊢ ((¬ 𝜑 ∨ 𝜓) → ¬ (𝜑 ∧ ¬ 𝜓))
Theorem	pm4.54dc 805	Theorem *4.54 of [WhiteheadRussell] p. 120, for decidable propositions. One form of DeMorgan's law. (Contributed by Jim Kingdon, 2-May-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → ((¬ 𝜑 ∧ 𝜓) ↔ ¬ (𝜑 ∨ ¬ 𝜓))))
Theorem	pm4.56 806	Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))
Theorem	oranim 807	Disjunction in terms of conjunction (DeMorgan's law). One direction of Theorem *4.57 of [WhiteheadRussell] p. 120. The converse does not hold intuitionistically but does hold in classical logic. (Contributed by Jim Kingdon, 25-Jul-2018.)
⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
Theorem	pm4.78i 808	Implication distributes over disjunction. One direction of Theorem *4.78 of [WhiteheadRussell] p. 121. The converse holds in classical logic. (Contributed by Jim Kingdon, 15-Jan-2018.)
⊢ (((𝜑 → 𝜓) ∨ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ∨ 𝜒)))
Theorem	pm4.79dc 809	Equivalence between a disjunction of two implications, and a conjunction and an implication. Based on theorem *4.79 of [WhiteheadRussell] p. 121 but with additional decidability antecedents. (Contributed by Jim Kingdon, 28-Mar-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → (((𝜓 → 𝜑) ∨ (𝜒 → 𝜑)) ↔ ((𝜓 ∧ 𝜒) → 𝜑))))
Theorem	pm5.17dc 810	Two ways of stating exclusive-or which are equivalent for a decidable proposition. Based on theorem *5.17 of [WhiteheadRussell] p. 124. (Contributed by Jim Kingdon, 16-Apr-2018.)
⊢ (DECID 𝜓 → (((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) ↔ (𝜑 ↔ ¬ 𝜓)))
Theorem	pm2.85dc 811	Reverse distribution of disjunction over implication, given decidability. Based on theorem *2.85 of [WhiteheadRussell] p. 108. (Contributed by Jim Kingdon, 1-Apr-2018.)
⊢ (DECID 𝜑 → (((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)) → (𝜑 ∨ (𝜓 → 𝜒))))
Theorem	orimdidc 812	Disjunction distributes over implication. The forward direction, pm2.76 721, is valid intuitionistically. The reverse direction holds if 𝜑 is decidable, as can be seen at pm2.85dc 811. (Contributed by Jim Kingdon, 1-Apr-2018.)
⊢ (DECID 𝜑 → ((𝜑 ∨ (𝜓 → 𝜒)) ↔ ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒))))
Theorem	pm2.26dc 813	Decidable proposition version of theorem *2.26 of [WhiteheadRussell] p. 104. (Contributed by Jim Kingdon, 20-Apr-2018.)
⊢ (DECID 𝜑 → (¬ 𝜑 ∨ ((𝜑 → 𝜓) → 𝜓)))
Theorem	pm4.81dc 814	Theorem *4.81 of [WhiteheadRussell] p. 122, for decidable propositions. This one needs a decidability condition, but compare with pm4.8 623 which holds for all propositions. (Contributed by Jim Kingdon, 4-Jul-2018.)
⊢ (DECID 𝜑 → ((¬ 𝜑 → 𝜑) ↔ 𝜑))
Theorem	pm5.11dc 815	A decidable proposition or its negation implies a second proposition. Based on theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 29-Mar-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 → 𝜓) ∨ (¬ 𝜑 → 𝜓))))
Theorem	pm5.12dc 816	Excluded middle with antecedents for a decidable consequent. Based on theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 30-Mar-2018.)
⊢ (DECID 𝜓 → ((𝜑 → 𝜓) ∨ (𝜑 → ¬ 𝜓)))
Theorem	pm5.14dc 817	A decidable proposition is implied by or implies other propositions. Based on theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 30-Mar-2018.)
⊢ (DECID 𝜓 → ((𝜑 → 𝜓) ∨ (𝜓 → 𝜒)))
Theorem	pm5.13dc 818	An implication holds in at least one direction, where one proposition is decidable. Based on theorem *5.13 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 30-Mar-2018.)
⊢ (DECID 𝜓 → ((𝜑 → 𝜓) ∨ (𝜓 → 𝜑)))
Theorem	pm5.55dc 819	A disjunction is equivalent to one of its disjuncts, given a decidable disjunct. Based on theorem *5.55 of [WhiteheadRussell] p. 125. (Contributed by Jim Kingdon, 30-Mar-2018.)
⊢ (DECID 𝜑 → (((𝜑 ∨ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∨ 𝜓) ↔ 𝜓)))
Theorem	peircedc 820	Peirce's theorem for a decidable proposition. This odd-looking theorem can be seen as an alternative to exmiddc 744, condc 749, or notnotrdc 751 in the sense of expressing the "difference" between an intuitionistic system of propositional calculus and a classical system. In intuitionistic logic, it only holds for decidable propositions. (Contributed by Jim Kingdon, 3-Jul-2018.)
⊢ (DECID 𝜑 → (((𝜑 → 𝜓) → 𝜑) → 𝜑))
Theorem	looinvdc 821	The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz, but where one of the propositions is decidable. Using dfor2dc 794, we can see that this expresses "disjunction commutes." Theorem *2.69 of [WhiteheadRussell] p. 108 (plus the decidability condition). (Contributed by NM, 12-Aug-2004.)
⊢ (DECID 𝜑 → (((𝜑 → 𝜓) → 𝜓) → ((𝜓 → 𝜑) → 𝜑)))
1.2.10  Testable propositions
Theorem	dftest 822	A proposition is testable iff its negative or double-negative is true. See Chapter 2 [Moschovakis] p. 2. Our notation for testability is DECID ¬ before the formula in question. For example, DECID ¬ 𝑥 = 𝑦 corresponds to "x = y is testable". (Contributed by David A. Wheeler, 13-Aug-2018.)
⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
Theorem	testbitestn 823	A proposition is testable iff its negation is testable. See also dcn 746 (which could be read as "Decidability implies testability"). (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (DECID ¬ 𝜑 ↔ DECID ¬ ¬ 𝜑)
Theorem	stabtestimpdc 824	"Stable and testable" is equivalent to decidable. (Contributed by David A. Wheeler, 13-Aug-2018.)
⊢ ((STAB 𝜑 ∧ DECID ¬ 𝜑) ↔ DECID 𝜑)
1.2.11  Miscellaneous theorems of propositional calculus
Theorem	pm5.21nd 825	Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.)
⊢ ((𝜑 ∧ 𝜓) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ (𝜃 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	pm5.35 826	Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ↔ 𝜒)))
Theorem	pm5.54dc 827	A conjunction is equivalent to one of its conjuncts, given a decidable conjunct. Based on theorem *5.54 of [WhiteheadRussell] p. 125. (Contributed by Jim Kingdon, 30-Mar-2018.)
⊢ (DECID 𝜑 → (((𝜑 ∧ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∧ 𝜓) ↔ 𝜓)))
Theorem	baib 828	Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜓 → (𝜑 ↔ 𝜒))
Theorem	baibr 829	Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜓 → (𝜒 ↔ 𝜑))
Theorem	rbaib 830	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜒 → (𝜑 ↔ 𝜓))
Theorem	rbaibr 831	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜒 → (𝜓 ↔ 𝜑))
Theorem	baibd 832	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))
Theorem	rbaibd 833	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒))
Theorem	pm5.44 834	Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) → ((𝜑 → 𝜒) ↔ (𝜑 → (𝜓 ∧ 𝜒))))
Theorem	pm5.6dc 835	Conjunction in antecedent versus disjunction in consequent, for a decidable proposition. Theorem *5.6 of [WhiteheadRussell] p. 125, with decidability condition added. The reverse implication holds for all propositions (see pm5.6r 836). (Contributed by Jim Kingdon, 2-Apr-2018.)
⊢ (DECID 𝜓 → (((𝜑 ∧ ¬ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 ∨ 𝜒))))
Theorem	pm5.6r 836	Conjunction in antecedent versus disjunction in consequent. One direction of Theorem *5.6 of [WhiteheadRussell] p. 125. If 𝜓 is decidable, the converse also holds (see pm5.6dc 835). (Contributed by Jim Kingdon, 4-Aug-2018.)
⊢ ((𝜑 → (𝜓 ∨ 𝜒)) → ((𝜑 ∧ ¬ 𝜓) → 𝜒))
Theorem	orcanai 837	Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)
Theorem	intnan 838	Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
⊢ ¬ 𝜑    ⇒   ⊢ ¬ (𝜓 ∧ 𝜑)
Theorem	intnanr 839	Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
⊢ ¬ 𝜑    ⇒   ⊢ ¬ (𝜑 ∧ 𝜓)
Theorem	intnand 840	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))
Theorem	intnanrd 841	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))
Theorem	dcan 842	A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∧ 𝜓)))
Theorem	dcor 843	A disjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 21-Apr-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))
Theorem	dcbi 844	An equivalence of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ↔ 𝜓)))
Theorem	annimdc 845	Express conjunction in terms of implication. The forward direction, annimim 782, is valid for all propositions, but as an equivalence, it requires a decidability condition. (Contributed by Jim Kingdon, 25-Apr-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))))
Theorem	pm4.55dc 846	Theorem *4.55 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 2-May-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (¬ 𝜑 ∧ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))))
Theorem	mpbiran 847	Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.) (Revised by NM, 9-Jan-2015.)
⊢ 𝜓    &   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 ↔ 𝜒)
Theorem	mpbiran2 848	Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) (Revised by NM, 9-Jan-2015.)
⊢ 𝜒    &   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	mpbir2an 849	Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) (Revised by NM, 9-Jan-2015.)
⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ 𝜑
Theorem	mpbi2and 850	Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mpbir2and 851	Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm5.62dc 852	Theorem *5.62 of [WhiteheadRussell] p. 125, for a decidable proposition. (Contributed by Jim Kingdon, 12-May-2018.)
⊢ (DECID 𝜓 → (((𝜑 ∧ 𝜓) ∨ ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓)))
Theorem	pm5.63dc 853	Theorem *5.63 of [WhiteheadRussell] p. 125, for a decidable proposition. (Contributed by Jim Kingdon, 12-May-2018.)
⊢ (DECID 𝜑 → ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ (¬ 𝜑 ∧ 𝜓))))
Theorem	bianfi 854	A wff conjoined with falsehood is false. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
⊢ ¬ 𝜑    ⇒   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))
Theorem	bianfd 855	A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))
Theorem	pm4.43 856	Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ ¬ 𝜓)))
Theorem	pm4.82 857	Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ↔ ¬ 𝜑)
Theorem	pm4.83dc 858	Theorem *4.83 of [WhiteheadRussell] p. 122, for decidable propositions. As with other case elimination theorems, like pm2.61dc 762, it only holds for decidable propositions. (Contributed by Jim Kingdon, 12-May-2018.)
⊢ (DECID 𝜑 → (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜓)) ↔ 𝜓))
Theorem	biantr 859	A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 18-Aug-1993.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜓)) → (𝜑 ↔ 𝜒))
Theorem	orbididc 860	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 861	Disjunction distributes over the biconditional, for a decidable proposition. Based on theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbididc 860. (Contributed by Jim Kingdon, 2-Apr-2018.)
⊢ (DECID 𝜒 → (((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) ↔ (𝜒 ∨ (𝜑 ↔ 𝜓))))
Theorem	bigolden 862	Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓)))
Theorem	anordc 863	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 671, holds for all propositions, but the equivalence only holds given decidability. (Contributed by Jim Kingdon, 21-Apr-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ 𝜓) ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓))))
Theorem	pm3.11dc 864	Theorem *3.11 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, pm3.1 671, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 22-Apr-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (¬ 𝜑 ∨ ¬ 𝜓) → (𝜑 ∧ 𝜓))))
Theorem	pm3.12dc 865	Theorem *3.12 of [WhiteheadRussell] p. 111, but for decidable propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓))))
Theorem	pm3.13dc 866	Theorem *3.13 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, pm3.14 670, holds for all propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓))))
Theorem	dn1dc 867	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 868	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 869	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 870	Removal of conjunct from one side of an equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 ↔ (𝜓 ∧ 𝜑))) → (𝜒 ↔ 𝜑))
Theorem	ccase 871	Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
⊢ ((𝜑 ∧ 𝜓) → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜓) → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏)
Theorem	ccased 872	Deduction for combining cases. (Contributed by NM, 9-May-2004.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜂))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂))    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → 𝜂))
Theorem	ccase2 873	Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
⊢ ((𝜑 ∧ 𝜓) → 𝜏)    &   ⊢ (𝜒 → 𝜏)    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏)
Theorem	niabn 874	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜓 → ((𝜒 ∧ 𝜓) ↔ ¬ 𝜑))
Theorem	dedlem0a 875	Alternate version of dedlema 876. (Contributed by NM, 2-Apr-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (𝜑 → (𝜓 ↔ ((𝜒 → 𝜑) → (𝜓 ∧ 𝜑))))
Theorem	dedlema 876	Lemma for iftrue 3336. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → (𝜓 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑))))
Theorem	dedlemb 877	Lemma for iffalse 3339. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (¬ 𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑))))
Theorem	pm4.42r 878	One direction of Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed by Jim Kingdon, 4-Aug-2018.)
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓)) → 𝜑)
Theorem	ninba 879	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜓 → (¬ 𝜑 ↔ (𝜒 ∧ 𝜓)))
Theorem	prlem1 880	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 881	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 882	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 883	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 884	Extend wff definition to include 3-way disjunction ('or').
wff (𝜑 ∨ 𝜓 ∨ 𝜒)
Syntax	w3a 885	Extend wff definition to include 3-way conjunction ('and').
wff (𝜑 ∧ 𝜓 ∧ 𝜒)
Definition	df-3or 886	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 684. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
Definition	df-3an 887	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 381. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
Theorem	3orass 888	Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
Theorem	3anass 889	Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
Theorem	3anrot 890	Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
Theorem	3orrot 891	Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))
Theorem	3ancoma 892	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
Theorem	3ancomb 893	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))
Theorem	3orcomb 894	Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓))
Theorem	3anrev 895	Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓 ∧ 𝜑))
Theorem	3anan32 896	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
Theorem	3anan12 897	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 898	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
Theorem	anandi3r 899	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜓)))
Theorem	3ioran 900	Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)
⊢ (¬ (𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒))