P. 11 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 1001-1100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	orabs 1001	Absorption of redundant internal disjunct. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 28-Feb-2014.)
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ 𝜑))
Theorem	oranabs 1002	Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.)
⊢ (((𝜑 ∨ ¬ 𝜓) ∧ 𝜓) ↔ (𝜑 ∧ 𝜓))
Theorem	pm5.61 1003	Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.)
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ 𝜓) ↔ (𝜑 ∧ ¬ 𝜓))
Theorem	pm5.6 1004	Conjunction in antecedent versus disjunction in consequent. Theorem *5.6 of [WhiteheadRussell] p. 125. (Contributed by NM, 8-Jun-1994.)
⊢ (((𝜑 ∧ ¬ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 ∨ 𝜒)))
Theorem	orcanai 1005	Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)
Theorem	pm4.79 1006	Theorem *4.79 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 27-Jun-2013.)
⊢ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜑)) ↔ ((𝜓 ∧ 𝜒) → 𝜑))
Theorem	pm5.53 1007	Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((((𝜑 ∨ 𝜓) ∨ 𝜒) → 𝜃) ↔ (((𝜑 → 𝜃) ∧ (𝜓 → 𝜃)) ∧ (𝜒 → 𝜃)))
Theorem	ordi 1008	Distributive law for disjunction. Theorem *4.41 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 28-Nov-2013.)
⊢ ((𝜑 ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒)))
Theorem	ordir 1009	Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒)))
Theorem	andi 1010	Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
Theorem	andir 1011	Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))
Theorem	orddi 1012	Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ 𝜃)) ↔ (((𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜃)) ∧ ((𝜓 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃))))
Theorem	anddi 1013	Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∨ 𝜓) ∧ (𝜒 ∨ 𝜃)) ↔ (((𝜑 ∧ 𝜒) ∨ (𝜑 ∧ 𝜃)) ∨ ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃))))
Theorem	pm5.17 1014	Theorem *5.17 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Jan-2013.)
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) ↔ (𝜑 ↔ ¬ 𝜓))
Theorem	pm5.15 1015	Theorem *5.15 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 15-Oct-2013.)
⊢ ((𝜑 ↔ 𝜓) ∨ (𝜑 ↔ ¬ 𝜓))
Theorem	pm5.16 1016	Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 17-Oct-2013.)
⊢ ¬ ((𝜑 ↔ 𝜓) ∧ (𝜑 ↔ ¬ 𝜓))
Theorem	xor 1017	Two ways to express exclusive disjunction (df-xor 1512). Theorem *5.22 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 22-Jan-2013.)
⊢ (¬ (𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑)))
Theorem	nbi2 1018	Two ways to express "exclusive or". (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Jan-2013.)
⊢ (¬ (𝜑 ↔ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)))
Theorem	xordi 1019	Conjunction distributes over exclusive-or, using ¬ (𝜑 ↔ 𝜓) to express exclusive-or. This is one way to interpret the distributive law of multiplication over addition in modulo 2 arithmetic. This is not necessarily true in intuitionistic logic, though anxordi 1526 does hold in it. (Contributed by NM, 3-Oct-2008.)
⊢ ((𝜑 ∧ ¬ (𝜓 ↔ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))
Theorem	pm5.54 1020	Theorem *5.54 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 7-Nov-2013.)
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∧ 𝜓) ↔ 𝜓))
Theorem	pm5.62 1021	Theorem *5.62 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 21-Jun-2005.)
⊢ (((𝜑 ∧ 𝜓) ∨ ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))
Theorem	pm5.63 1022	Theorem *5.63 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
⊢ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ (¬ 𝜑 ∧ 𝜓)))
Theorem	niabn 1023	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜓 → ((𝜒 ∧ 𝜓) ↔ ¬ 𝜑))
Theorem	ninba 1024	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜓 → (¬ 𝜑 ↔ (𝜒 ∧ 𝜓)))
Theorem	pm4.43 1025	Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ ¬ 𝜓)))
Theorem	pm4.82 1026	Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ↔ ¬ 𝜑)
Theorem	pm4.83 1027	Theorem *4.83 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜓)) ↔ 𝜓)
Theorem	pclem6 1028	Negation inferred from embedded conjunct. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Nov-2012.)
⊢ ((𝜑 ↔ (𝜓 ∧ ¬ 𝜑)) → ¬ 𝜓)
Theorem	bigolden 1029	Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓)))
Theorem	pm5.71 1030	Theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.)
⊢ ((𝜓 → ¬ 𝜒) → (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ 𝜒)))
Theorem	pm5.75 1031	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.) (Proof shortened by Kyle Wyonch, 12-Feb-2021.)
⊢ (((𝜒 → ¬ 𝜓) ∧ (𝜑 ↔ (𝜓 ∨ 𝜒))) → ((𝜑 ∧ ¬ 𝜓) ↔ 𝜒))
Theorem	ecase2d 1032	Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Sep-2024.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))    &   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜃))    &   ⊢ (𝜑 → (𝜏 ∨ (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	ecase3 1033	Inference for elimination by cases. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (¬ (𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	ecase 1034	Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.)
⊢ (¬ 𝜑 → 𝜒)    &   ⊢ (¬ 𝜓 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	ecase3d 1035	Deduction for elimination by cases. (Contributed by NM, 2-May-1996.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → (¬ (𝜓 ∨ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	ecased 1036	Deduction for elimination by cases. (Contributed by NM, 8-Oct-2012.)
⊢ (𝜑 → (¬ 𝜓 → 𝜃))    &   ⊢ (𝜑 → (¬ 𝜒 → 𝜃))    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	ecase3ad 1037	Deduction for elimination by cases. (Contributed by NM, 24-May-2013.) (Proof shortened by Wolf Lammen, 20-Sep-2024.)
⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → ((¬ 𝜓 ∧ ¬ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	ccase 1038	Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
⊢ ((𝜑 ∧ 𝜓) → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜓) → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏)
Theorem	ccased 1039	Deduction for combining cases. (Contributed by NM, 9-May-2004.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜂))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂))    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → 𝜂))
Theorem	ccase2 1040	Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
⊢ ((𝜑 ∧ 𝜓) → 𝜏)    &   ⊢ (𝜒 → 𝜏)    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏)
Theorem	4cases 1041	Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 25-Oct-2003.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)    &   ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	4casesdan 1042	Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 19-Mar-2013.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    &   ⊢ ((𝜑 ∧ (𝜓 ∧ ¬ 𝜒)) → 𝜃)    &   ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ 𝜒)) → 𝜃)    &   ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ ¬ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	cases 1043	Case disjunction according to the value of 𝜑. (Contributed by NM, 25-Apr-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (¬ 𝜑 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜓 ↔ ((𝜑 ∧ 𝜒) ∨ (¬ 𝜑 ∧ 𝜃)))
Theorem	dedlem0a 1044	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 1045	Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.)
⊢ (¬ 𝜑 → (𝜓 ↔ ((𝜓 → 𝜑) → (𝜒 ∧ 𝜑))))
Theorem	dedlema 1046	Lemma for weak deduction theorem. See also ifptru 1075. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → (𝜓 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑))))
Theorem	dedlemb 1047	Lemma for weak deduction theorem. See also ifpfal 1076. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (¬ 𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑))))
Theorem	cases2 1048	Case disjunction according to the value of 𝜑. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 28-Feb-2022.)
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)))
Theorem	cases2ALT 1049	Alternate proof of cases2 1048, not using dedlema 1046 or dedlemb 1047. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 2-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)))
Theorem	dfbi3 1050	An alternate definition of the biconditional. Theorem *5.23 of [WhiteheadRussell] p. 124. (Contributed by NM, 27-Jun-2002.) (Proof shortened by Wolf Lammen, 3-Nov-2013.) (Proof shortened by NM, 29-Oct-2021.)
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)))
Theorem	pm5.24 1051	Theorem *5.24 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑)))
Theorem	4exmid 1052	The disjunction of the four possible combinations of two wffs and their negations is always true. A four-way excluded middle (see exmid 895). (Contributed by David Abernethy, 28-Jan-2014.) (Proof shortened by NM, 29-Oct-2021.)
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) ∨ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑)))
Theorem	consensus 1053	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 1054	Theorem *4.42 of [WhiteheadRussell] p. 119. See also ifpid 1077. (Contributed by Roy F. Longton, 21-Jun-2005.)
⊢ (𝜑 ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓)))
Theorem	prlem1 1055	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 1056	A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∧ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ 𝜃))))
Theorem	oplem1 1057	A specialized lemma for set theory (ordered pair theorem). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Wolf Lammen, 8-Dec-2012.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    &   ⊢ (𝜑 → (𝜃 ∨ 𝜏))    &   ⊢ (𝜓 ↔ 𝜃)    &   ⊢ (𝜒 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	dn1 1058	A single axiom for Boolean algebra known as DN1. See McCune, Veroff, Fitelson, Harris, Feist, Wos, Short single axioms for Boolean algebra, Journal of Automated Reasoning, 29(1):1--16, 2002. (https://www.cs.unm.edu/~mccune/papers/basax/v12.pdf). (Contributed by Jeff Hankins, 3-Jul-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
⊢ (¬ (¬ (¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))) ↔ 𝜒)
Theorem	bianir 1059	A closed form of mpbir 231, analogous to pm2.27 42 (assertion). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Roger Witte, 17-Aug-2020.)
⊢ ((𝜑 ∧ (𝜓 ↔ 𝜑)) → 𝜓)
Theorem	jaoi2 1060	Inference removing a negated conjunct in a disjunction of an antecedent if this conjunct is part of the disjunction. (Contributed by Alexander van der Vekens, 3-Nov-2017.) (Proof shortened by Wolf Lammen, 21-Sep-2018.)
⊢ ((𝜑 ∨ (¬ 𝜑 ∧ 𝜒)) → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → 𝜓)
Theorem	jaoi3 1061	Inference separating a disjunct of an antecedent. (Contributed by Alexander van der Vekens, 25-May-2018.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((¬ 𝜑 ∧ 𝜒) → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → 𝜓)
Theorem	ornld 1062	Selecting one statement from a disjunction if one of the disjuncted statements is false. (Contributed by AV, 6-Sep-2018.) (Proof shortened by AV, 13-Oct-2018.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
⊢ (𝜑 → (((𝜑 → (𝜃 ∨ 𝜏)) ∧ ¬ 𝜃) → 𝜏))
1.2.9  The conditional operator for propositions This subsection introduces the conditional operator for propositions, denoted by if-(𝜑, 𝜓, 𝜒) (see df-ifp 1064). It is the analogue for propositions of the conditional operator for classes, denoted by if(𝜑, 𝐴, 𝐵) (see df-if 4526).
Syntax	wif 1063	Extend wff notation to include the conditional operator for propositions.
wff if-(𝜑, 𝜓, 𝜒)
Definition	df-ifp 1064	Definition of the conditional operator for propositions. The expression if-(𝜑, 𝜓, 𝜒) is read "if 𝜑 then 𝜓 else 𝜒". See dfifp2 1065, dfifp3 1066, dfifp4 1067, dfifp5 1068, dfifp6 1069 and dfifp7 1070 for alternate definitions. This definition (in the form of dfifp2 1065) appears in Section II.24 of [Church] p. 129 (Definition D12 page 132), where it is called "conditioned disjunction". Church's [𝜓, 𝜑, 𝜒] corresponds to our if-(𝜑, 𝜓, 𝜒) (note the permutation of the first two variables). This form was chosen as the definition rather than dfifp2 1065 for compatibility with intuitionistic logic development: with this form, it is clear that if-(𝜑, 𝜓, 𝜒) implies decidability of 𝜑, which is most often what is wanted. Church uses the conditional operator as an intermediate step to prove completeness of some systems of connectives. The first result is that the system {if-, ⊤, ⊥} is complete: for the induction step, consider a formula of n+1 variables; single out one variable, say 𝜑; when one sets 𝜑 to True (resp. False), then what remains is a formula of n variables, so by the induction hypothesis it is equivalent to a formula using only the connectives if-, ⊤, ⊥, say 𝜓 (resp. 𝜒); therefore, the formula if-(𝜑, 𝜓, 𝜒) is equivalent to the initial formula of n+1 variables. Now, since { → , ¬ } and similar systems suffice to express the connectives if-, ⊤, ⊥, they are also complete. (Contributed by BJ, 22-Jun-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)))
Theorem	dfifp2 1065	Alternate definition of the conditional operator for propositions. The value of if-(𝜑, 𝜓, 𝜒) is "if 𝜑 then 𝜓, and if not 𝜑 then 𝜒". This is the definition used in Section II.24 of [Church] p. 129 (Definition D12 page 132) (see comment of df-ifp 1064). (Contributed by BJ, 22-Jun-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)))
Theorem	dfifp3 1066	Alternate definition of the conditional operator for propositions. (Contributed by BJ, 30-Sep-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ (𝜑 ∨ 𝜒)))
Theorem	dfifp4 1067	Alternate definition of the conditional operator for propositions. (Contributed by BJ, 30-Sep-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒)))
Theorem	dfifp5 1068	Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (¬ 𝜑 → 𝜒)))
Theorem	dfifp6 1069	Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ ¬ (𝜒 → 𝜑)))
Theorem	dfifp7 1070	Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜒 → 𝜑) → (𝜑 ∧ 𝜓)))
Theorem	ifpdfbi 1071	Define the biconditional as conditional logic operator. (Contributed by RP, 20-Apr-2020.) (Proof shortened by Wolf Lammen, 30-Apr-2024.)
⊢ ((𝜑 ↔ 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜓))
Theorem	anifp 1072	The conditional operator is implied by the conjunction of its possible outputs. Dual statement of ifpor 1073. (Contributed by BJ, 30-Sep-2019.)
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒))
Theorem	ifpor 1073	The conditional operator implies the disjunction of its possible outputs. Dual statement of anifp 1072. (Contributed by BJ, 1-Oct-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) → (𝜓 ∨ 𝜒))
Theorem	ifpn 1074	Conditional operator for the negation of a proposition. (Contributed by BJ, 30-Sep-2019.) (Proof shortened by Wolf Lammen, 5-May-2024.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ if-(¬ 𝜑, 𝜒, 𝜓))
Theorem	ifptru 1075	Value of the conditional operator for propositions when its first argument is true. Analogue for propositions of iftrue 4531. This is essentially dedlema 1046. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 10-Jul-2020.)
⊢ (𝜑 → (if-(𝜑, 𝜓, 𝜒) ↔ 𝜓))
Theorem	ifpfal 1076	Value of the conditional operator for propositions when its first argument is false. Analogue for propositions of iffalse 4534. This is essentially dedlemb 1047. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 25-Jun-2020.)
⊢ (¬ 𝜑 → (if-(𝜑, 𝜓, 𝜒) ↔ 𝜒))
Theorem	ifpid 1077	Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of ifid 4566. This is essentially pm4.42 1054. (Contributed by BJ, 20-Sep-2019.)
⊢ (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓)
Theorem	casesifp 1078	Version of cases 1043 expressed using if-. Case disjunction according to the value of 𝜑. One can see this as a proof that the two hypotheses characterize the conditional operator for propositions. For the converses, see ifptru 1075 and ifpfal 1076. (Contributed by BJ, 20-Sep-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (¬ 𝜑 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜓 ↔ if-(𝜑, 𝜒, 𝜃))
Theorem	ifpbi123d 1079	Equivalence deduction for conditional operator for propositions. (Contributed by AV, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 17-Apr-2024.)
⊢ (𝜑 → (𝜓 ↔ 𝜏))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜂))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜁))    ⇒   ⊢ (𝜑 → (if-(𝜓, 𝜒, 𝜃) ↔ if-(𝜏, 𝜂, 𝜁)))
Theorem	ifpbi23d 1080	Equivalence deduction for conditional operator for propositions. Convenience theorem for a frequent case. (Contributed by Wolf Lammen, 28-Apr-2024.)
⊢ (𝜑 → (𝜒 ↔ 𝜂))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜁))    ⇒   ⊢ (𝜑 → (if-(𝜓, 𝜒, 𝜃) ↔ if-(𝜓, 𝜂, 𝜁)))
Theorem	ifpimpda 1081	Separation of the values of the conditional operator for propositions. (Contributed by AV, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 27-Feb-2021.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜃)    ⇒   ⊢ (𝜑 → if-(𝜓, 𝜒, 𝜃))
Theorem	1fpid3 1082	The value of the conditional operator for propositions is its third argument if the first and second argument imply the third argument. (Contributed by AV, 4-Apr-2021.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (if-(𝜑, 𝜓, 𝜒) → 𝜒)
1.2.10  The weak deduction theorem for propositional calculus This subsection contains a few results related to the weak deduction theorem in propositional calculus. For the weak deduction theorem in set theory, see the section beginning with dedth 4584. For more information on the weak deduction theorem, see the Weak Deduction Theorem page mmdeduction.html 4584.
Theorem	elimh 1083	Hypothesis builder for the weak deduction theorem. For more information, see the Weak Deduction Theorem page mmdeduction.html. (Contributed by NM, 26-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) Commute consequent. (Revised by Steven Nguyen, 27-Apr-2023.)
⊢ ((if-(𝜒, 𝜑, 𝜓) ↔ 𝜑) → (𝜏 ↔ 𝜒))    &   ⊢ ((if-(𝜒, 𝜑, 𝜓) ↔ 𝜓) → (𝜏 ↔ 𝜃))    &   ⊢ 𝜃    ⇒   ⊢ 𝜏
Theorem	dedt 1084	The weak deduction theorem. For more information, see the Weak Deduction Theorem page mmdeduction.html. (Contributed by NM, 26-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) Commute consequent. (Revised by Steven Nguyen, 27-Apr-2023.)
⊢ ((if-(𝜒, 𝜑, 𝜓) ↔ 𝜑) → (𝜏 ↔ 𝜃))    &   ⊢ 𝜏    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	con3ALT 1085	Proof of con3 153 from its associated inference con3i 154 that illustrates the use of the weak deduction theorem dedt 1084. (Contributed by NM, 27-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) Revised dedt 1084 and elimh 1083. (Revised by Steven Nguyen, 27-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))
1.2.11  Abbreviated conjunction and disjunction of three wff's
Syntax	w3o 1086	Extend wff definition to include three-way disjunction ('or').
wff (𝜑 ∨ 𝜓 ∨ 𝜒)
Syntax	w3a 1087	Extend wff definition to include three-way conjunction ('and').
wff (𝜑 ∧ 𝜓 ∧ 𝜒)
Definition	df-3or 1088	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 922. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
Definition	df-3an 1089	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 468. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
Theorem	3orass 1090	Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
Theorem	3orel1 1091	Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.)
⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜓 ∨ 𝜒)))
Theorem	3orrot 1092	Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))
Theorem	3orcoma 1093	Commutation law for triple disjunction. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜑 ∨ 𝜒))
Theorem	3orcomb 1094	Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.) (Proof shortened by Wolf Lammen, 8-Apr-2022.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓))
Theorem	3anass 1095	Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
Theorem	3anan12 1096	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised to shorten 3ancoma 1098 by Wolf Lammen, 5-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
Theorem	3anan32 1097	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
Theorem	3ancoma 1098	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 5-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
Theorem	3ancomb 1099	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Revised to shorten 3anrot 1100 by Wolf Lammen, 9-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))
Theorem	3anrot 1100	Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.) (Proof shortened by Wolf Lammen, 9-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))