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	pm5.61 1001	Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.)
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ 𝜓) ↔ (𝜑 ∧ ¬ 𝜓))
Theorem	pm5.6 1002	Conjunction in antecedent versus disjunction in consequent. Theorem *5.6 of [WhiteheadRussell] p. 125. (Contributed by NM, 8-Jun-1994.)
⊢ (((𝜑 ∧ ¬ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 ∨ 𝜒)))
Theorem	orcanai 1003	Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)
Theorem	pm4.79 1004	Theorem *4.79 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 27-Jun-2013.)
⊢ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜑)) ↔ ((𝜓 ∧ 𝜒) → 𝜑))
Theorem	pm5.53 1005	Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((((𝜑 ∨ 𝜓) ∨ 𝜒) → 𝜃) ↔ (((𝜑 → 𝜃) ∧ (𝜓 → 𝜃)) ∧ (𝜒 → 𝜃)))
Theorem	ordi 1006	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 1007	Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒)))
Theorem	andi 1008	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 1009	Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))
Theorem	orddi 1010	Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ 𝜃)) ↔ (((𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜃)) ∧ ((𝜓 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃))))
Theorem	anddi 1011	Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∨ 𝜓) ∧ (𝜒 ∨ 𝜃)) ↔ (((𝜑 ∧ 𝜒) ∨ (𝜑 ∧ 𝜃)) ∨ ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃))))
Theorem	pm5.17 1012	Theorem *5.17 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Jan-2013.)
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) ↔ (𝜑 ↔ ¬ 𝜓))
Theorem	pm5.15 1013	Theorem *5.15 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 15-Oct-2013.)
⊢ ((𝜑 ↔ 𝜓) ∨ (𝜑 ↔ ¬ 𝜓))
Theorem	pm5.16 1014	Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 17-Oct-2013.)
⊢ ¬ ((𝜑 ↔ 𝜓) ∧ (𝜑 ↔ ¬ 𝜓))
Theorem	xor 1015	Two ways to express exclusive disjunction (df-xor 1508). Theorem *5.22 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 22-Jan-2013.)
⊢ (¬ (𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑)))
Theorem	nbi2 1016	Two ways to express "exclusive or". (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Jan-2013.)
⊢ (¬ (𝜑 ↔ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)))
Theorem	xordi 1017	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 1524 does hold in it. (Contributed by NM, 3-Oct-2008.)
⊢ ((𝜑 ∧ ¬ (𝜓 ↔ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))
Theorem	pm5.54 1018	Theorem *5.54 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 7-Nov-2013.)
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∧ 𝜓) ↔ 𝜓))
Theorem	pm5.62 1019	Theorem *5.62 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 21-Jun-2005.)
⊢ (((𝜑 ∧ 𝜓) ∨ ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))
Theorem	pm5.63 1020	Theorem *5.63 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
⊢ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ (¬ 𝜑 ∧ 𝜓)))
Theorem	niabn 1021	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜓 → ((𝜒 ∧ 𝜓) ↔ ¬ 𝜑))
Theorem	ninba 1022	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜓 → (¬ 𝜑 ↔ (𝜒 ∧ 𝜓)))
Theorem	pm4.43 1023	Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ ¬ 𝜓)))
Theorem	pm4.82 1024	Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ↔ ¬ 𝜑)
Theorem	pm4.83 1025	Theorem *4.83 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜓)) ↔ 𝜓)
Theorem	pclem6 1026	Negation inferred from embedded conjunct. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Nov-2012.)
⊢ ((𝜑 ↔ (𝜓 ∧ ¬ 𝜑)) → ¬ 𝜓)
Theorem	bigolden 1027	Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓)))
Theorem	pm5.71 1028	Theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.)
⊢ ((𝜓 → ¬ 𝜒) → (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ 𝜒)))
Theorem	pm5.75 1029	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 1030	Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Sep-2024.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))    &   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜃))    &   ⊢ (𝜑 → (𝜏 ∨ (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	ecase2dOLD 1031	Obsolete version of ecase2d 1030 as of 19-Sep-2024. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Dec-2012.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))    &   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜃))    &   ⊢ (𝜑 → (𝜏 ∨ (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	ecase3 1032	Inference for elimination by cases. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (¬ (𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	ecase 1033	Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.)
⊢ (¬ 𝜑 → 𝜒)    &   ⊢ (¬ 𝜓 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	ecase3d 1034	Deduction for elimination by cases. (Contributed by NM, 2-May-1996.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → (¬ (𝜓 ∨ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	ecased 1035	Deduction for elimination by cases. (Contributed by NM, 8-Oct-2012.)
⊢ (𝜑 → (¬ 𝜓 → 𝜃))    &   ⊢ (𝜑 → (¬ 𝜒 → 𝜃))    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	ecase3ad 1036	Deduction for elimination by cases. (Contributed by NM, 24-May-2013.) (Proof shortened by Wolf Lammen, 20-Sep-2024.)
⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → ((¬ 𝜓 ∧ ¬ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	ecase3adOLD 1037	Obsolete version of ecase3ad 1036 as of 20-Sep-2024. (Contributed by NM, 24-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → ((¬ 𝜓 ∧ ¬ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
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 1076. (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 1077. (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 1078. (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 234, 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 4440).
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	ifpnOLD 1075	Obsolete version of ifpn 1074 as of 5-May-2024. (Contributed by BJ, 30-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ if-(¬ 𝜑, 𝜒, 𝜓))
Theorem	ifptru 1076	Value of the conditional operator for propositions when its first argument is true. Analogue for propositions of iftrue 4445. This is essentially dedlema 1046. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 10-Jul-2020.)
⊢ (𝜑 → (if-(𝜑, 𝜓, 𝜒) ↔ 𝜓))
Theorem	ifpfal 1077	Value of the conditional operator for propositions when its first argument is false. Analogue for propositions of iffalse 4448. This is essentially dedlemb 1047. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 25-Jun-2020.)
⊢ (¬ 𝜑 → (if-(𝜑, 𝜓, 𝜒) ↔ 𝜒))
Theorem	ifpid 1078	Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of ifid 4479. This is essentially pm4.42 1054. (Contributed by BJ, 20-Sep-2019.)
⊢ (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓)
Theorem	casesifp 1079	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 1076 and ifpfal 1077. (Contributed by BJ, 20-Sep-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (¬ 𝜑 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜓 ↔ if-(𝜑, 𝜒, 𝜃))
Theorem	ifpbi123d 1080	Equivalence deduction for conditional operator for propositions. (Contributed by AV, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 17-Apr-2024.)
⊢ (𝜑 → (𝜓 ↔ 𝜏))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜂))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜁))    ⇒   ⊢ (𝜑 → (if-(𝜓, 𝜒, 𝜃) ↔ if-(𝜏, 𝜂, 𝜁)))
Theorem	ifpbi123dOLD 1081	Obsolete version of ifpbi123d 1080 as of 17-Apr-2024. (Contributed by AV, 30-Dec-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 ↔ 𝜏))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜂))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜁))    ⇒   ⊢ (𝜑 → (if-(𝜓, 𝜒, 𝜃) ↔ if-(𝜏, 𝜂, 𝜁)))
Theorem	ifpbi23d 1082	Equivalence deduction for conditional operator for propositions. Convenience theorem for a frequent case. (Contributed by Wolf Lammen, 28-Apr-2024.)
⊢ (𝜑 → (𝜒 ↔ 𝜂))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜁))    ⇒   ⊢ (𝜑 → (if-(𝜓, 𝜒, 𝜃) ↔ if-(𝜓, 𝜂, 𝜁)))
Theorem	ifpimpda 1083	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 1084	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 4497. For more information on the weak deduction theorem, see the Weak Deduction Theorem page mmdeduction.html 4497.
Theorem	elimh 1085	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 1086	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 1087	Proof of con3 156 from its associated inference con3i 157 that illustrates the use of the weak deduction theorem dedt 1086. (Contributed by NM, 27-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) Revised dedt 1086 and elimh 1085. (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 1088	Extend wff definition to include three-way disjunction ('or').
wff (𝜑 ∨ 𝜓 ∨ 𝜒)
Syntax	w3a 1089	Extend wff definition to include three-way conjunction ('and').
wff (𝜑 ∧ 𝜓 ∧ 𝜒)
Definition	df-3or 1090	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 1091	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 472. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
Theorem	3orass 1092	Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
Theorem	3orel1 1093	Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.)
⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜓 ∨ 𝜒)))
Theorem	3orrot 1094	Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))
Theorem	3orcoma 1095	Commutation law for triple disjunction. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜑 ∨ 𝜒))
Theorem	3orcomb 1096	Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.) (Proof shortened by Wolf Lammen, 8-Apr-2022.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓))
Theorem	3anass 1097	Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
Theorem	3anan12 1098	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 1100 by Wolf Lammen, 5-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
Theorem	3anan32 1099	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
Theorem	3ancoma 1100	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 5-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))