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	pm4.56 1001	Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))
Theorem	oran 1002	Disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ ((𝜑 ∨ 𝜓) ↔ ¬ (¬ 𝜑 ∧ ¬ 𝜓))
Theorem	pm4.57 1003	Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 ∧ ¬ 𝜓) ↔ (𝜑 ∨ 𝜓))
Theorem	pm3.1 1004	Theorem *3.1 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∧ 𝜓) → ¬ (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	pm3.11 1005	Theorem *3.11 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 ∨ ¬ 𝜓) → (𝜑 ∧ 𝜓))
Theorem	pm3.12 1006	Theorem *3.12 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓))
Theorem	pm3.13 1007	Theorem *3.13 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	pm3.14 1008	Theorem *3.14 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
Theorem	pm4.44 1009	Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∨ (𝜑 ∧ 𝜓)))
Theorem	pm4.45 1010	Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∧ (𝜑 ∨ 𝜓)))
Theorem	orabs 1011	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 1012	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 1013	Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.)
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ 𝜓) ↔ (𝜑 ∧ ¬ 𝜓))
Theorem	pm5.6 1014	Conjunction in antecedent versus disjunction in consequent. Theorem *5.6 of [WhiteheadRussell] p. 125. (Contributed by NM, 8-Jun-1994.)
⊢ (((𝜑 ∧ ¬ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 ∨ 𝜒)))
Theorem	orcanai 1015	Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)
Theorem	pm4.79 1016	Theorem *4.79 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 27-Jun-2013.)
⊢ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜑)) ↔ ((𝜓 ∧ 𝜒) → 𝜑))
Theorem	pm5.53 1017	Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((((𝜑 ∨ 𝜓) ∨ 𝜒) → 𝜃) ↔ (((𝜑 → 𝜃) ∧ (𝜓 → 𝜃)) ∧ (𝜒 → 𝜃)))
Theorem	ordi 1018	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 1019	Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒)))
Theorem	andi 1020	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 1021	Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))
Theorem	orddi 1022	Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ 𝜃)) ↔ (((𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜃)) ∧ ((𝜓 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃))))
Theorem	anddi 1023	Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∨ 𝜓) ∧ (𝜒 ∨ 𝜃)) ↔ (((𝜑 ∧ 𝜒) ∨ (𝜑 ∧ 𝜃)) ∨ ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃))))
Theorem	pm5.17 1024	Theorem *5.17 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Jan-2013.)
⊢ (((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) ↔ (𝜑 ↔ ¬ 𝜓))
Theorem	pm5.15 1025	Theorem *5.15 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 15-Oct-2013.)
⊢ ((𝜑 ↔ 𝜓) ∨ (𝜑 ↔ ¬ 𝜓))
Theorem	pm5.16 1026	Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 17-Oct-2013.)
⊢ ¬ ((𝜑 ↔ 𝜓) ∧ (𝜑 ↔ ¬ 𝜓))
Theorem	xor 1027	Two ways to express exclusive disjunction (df-xor 1531). Theorem *5.22 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 22-Jan-2013.)
⊢ (¬ (𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑)))
Theorem	nbi2 1028	Two ways to express "exclusive or". (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Jan-2013.)
⊢ (¬ (𝜑 ↔ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)))
Theorem	xordi 1029	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 1545 does hold in it. (Contributed by NM, 3-Oct-2008.)
⊢ ((𝜑 ∧ ¬ (𝜓 ↔ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))
Theorem	pm5.54 1030	Theorem *5.54 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 7-Nov-2013.)
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∧ 𝜓) ↔ 𝜓))
Theorem	pm5.62 1031	Theorem *5.62 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 21-Jun-2005.)
⊢ (((𝜑 ∧ 𝜓) ∨ ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))
Theorem	pm5.63 1032	Theorem *5.63 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
⊢ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ (¬ 𝜑 ∧ 𝜓)))
Theorem	niabn 1033	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜓 → ((𝜒 ∧ 𝜓) ↔ ¬ 𝜑))
Theorem	ninba 1034	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜓 → (¬ 𝜑 ↔ (𝜒 ∧ 𝜓)))
Theorem	pm4.43 1035	Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ ¬ 𝜓)))
Theorem	pm4.82 1036	Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ↔ ¬ 𝜑)
Theorem	pm4.83 1037	Theorem *4.83 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜓)) ↔ 𝜓)
Theorem	pclem6 1038	Negation inferred from embedded conjunct. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Nov-2012.)
⊢ ((𝜑 ↔ (𝜓 ∧ ¬ 𝜑)) → ¬ 𝜓)
Theorem	bigolden 1039	Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓)))
Theorem	pm5.71 1040	Theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.)
⊢ ((𝜓 → ¬ 𝜒) → (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ 𝜒)))
Theorem	pm5.75 1041	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 1042	Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Sep-2024.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))    &   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜃))    &   ⊢ (𝜑 → (𝜏 ∨ (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	ecase3 1043	Inference for elimination by cases. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (¬ (𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	ecase 1044	Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.)
⊢ (¬ 𝜑 → 𝜒)    &   ⊢ (¬ 𝜓 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	ecase3d 1045	Deduction for elimination by cases. (Contributed by NM, 2-May-1996.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → (¬ (𝜓 ∨ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	ecased 1046	Deduction for elimination by cases. (Contributed by NM, 8-Oct-2012.)
⊢ (𝜑 → (¬ 𝜓 → 𝜃))    &   ⊢ (𝜑 → (¬ 𝜒 → 𝜃))    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	ecase3ad 1047	Deduction for elimination by cases. (Contributed by NM, 24-May-2013.) (Proof shortened by Wolf Lammen, 20-Sep-2024.)
⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → ((¬ 𝜓 ∧ ¬ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	ccase 1048	Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
⊢ ((𝜑 ∧ 𝜓) → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜓) → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏)
Theorem	ccased 1049	Deduction for combining cases. (Contributed by NM, 9-May-2004.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜂))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂))    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → 𝜂))
Theorem	ccase2 1050	Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
⊢ ((𝜑 ∧ 𝜓) → 𝜏)    &   ⊢ (𝜒 → 𝜏)    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏)
Theorem	4cases 1051	Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 25-Oct-2003.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)    &   ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	4casesdan 1052	Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 19-Mar-2013.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    &   ⊢ ((𝜑 ∧ (𝜓 ∧ ¬ 𝜒)) → 𝜃)    &   ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ 𝜒)) → 𝜃)    &   ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ ¬ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	cases 1053	Case disjunction according to the value of 𝜑. (Contributed by NM, 25-Apr-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (¬ 𝜑 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜓 ↔ ((𝜑 ∧ 𝜒) ∨ (¬ 𝜑 ∧ 𝜃)))
Theorem	dedlem0a 1054	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 1055	Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.)
⊢ (¬ 𝜑 → (𝜓 ↔ ((𝜓 → 𝜑) → (𝜒 ∧ 𝜑))))
Theorem	dedlema 1056	Lemma for weak deduction theorem. See also ifptru 1085. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → (𝜓 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑))))
Theorem	dedlemb 1057	Lemma for weak deduction theorem. See also ifpfal 1086. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (¬ 𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑))))
Theorem	cases2 1058	Case disjunction according to the value of 𝜑. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 28-Feb-2022.)
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)))
Theorem	cases2ALT 1059	Alternate proof of cases2 1058, not using dedlema 1056 or dedlemb 1057. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 2-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)))
Theorem	dfbi3 1060	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 1061	Theorem *5.24 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑)))
Theorem	4exmid 1062	The disjunction of the four possible combinations of two wffs and their negations is always true. A four-way excluded middle (see exmid 905). (Contributed by David Abernethy, 28-Jan-2014.) (Proof shortened by NM, 29-Oct-2021.)
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) ∨ ((𝜑 ∧ ¬ 𝜓) ∨ (𝜓 ∧ ¬ 𝜑)))
Theorem	consensus 1063	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 1064	Theorem *4.42 of [WhiteheadRussell] p. 119. See also ifpid 1087. (Contributed by Roy F. Longton, 21-Jun-2005.)
⊢ (𝜑 ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓)))
Theorem	prlem1 1065	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 1066	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 1067	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 1068	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 1069	A closed form of mpbir 233, analogous to pm2.27 42 (assertion). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Roger Witte, 17-Aug-2020.)
⊢ ((𝜑 ∧ (𝜓 ↔ 𝜑)) → 𝜓)
Theorem	jaoi2 1070	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 1071	Inference separating a disjunct of an antecedent. (Contributed by Alexander van der Vekens, 25-May-2018.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((¬ 𝜑 ∧ 𝜒) → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → 𝜓)
Theorem	ornld 1072	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 1074). It is the analogue for propositions of the conditional operator for classes, denoted by if(𝜑, 𝐴, 𝐵) (see df-if 4480).
Syntax	wif 1073	Extend wff notation to include the conditional operator for propositions.
wff if-(𝜑, 𝜓, 𝜒)
Definition	df-ifp 1074	Definition of the conditional operator for propositions. The expression if-(𝜑, 𝜓, 𝜒) is read "if 𝜑 then 𝜓 else 𝜒". See dfifp2 1075, dfifp3 1076, dfifp4 1077, dfifp5 1078, dfifp6 1079 and dfifp7 1080 for alternate definitions. This definition (in the form of dfifp2 1075) 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 1075 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 1075	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 1074). (Contributed by BJ, 22-Jun-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)))
Theorem	dfifp3 1076	Alternate definition of the conditional operator for propositions. (Contributed by BJ, 30-Sep-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ (𝜑 ∨ 𝜒)))
Theorem	dfifp4 1077	Alternate definition of the conditional operator for propositions. (Contributed by BJ, 30-Sep-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒)))
Theorem	dfifp5 1078	Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (¬ 𝜑 → 𝜒)))
Theorem	dfifp6 1079	Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ ¬ (𝜒 → 𝜑)))
Theorem	dfifp7 1080	Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜒 → 𝜑) → (𝜑 ∧ 𝜓)))
Theorem	ifpdfbi 1081	Define the biconditional as conditional logic operator. (Contributed by RP, 20-Apr-2020.) (Proof shortened by Wolf Lammen, 30-Apr-2024.)
⊢ ((𝜑 ↔ 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜓))
Theorem	anifp 1082	The conditional operator is implied by the conjunction of its possible outputs. Dual statement of ifpor 1083. (Contributed by BJ, 30-Sep-2019.)
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒))
Theorem	ifpor 1083	The conditional operator implies the disjunction of its possible outputs. Dual statement of anifp 1082. (Contributed by BJ, 1-Oct-2019.)
⊢ (if-(𝜑, 𝜓, 𝜒) → (𝜓 ∨ 𝜒))
Theorem	ifpn 1084	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 1085	Value of the conditional operator for propositions when its first argument is true. Analogue for propositions of iftrue 4485. This is essentially dedlema 1056. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 10-Jul-2020.)
⊢ (𝜑 → (if-(𝜑, 𝜓, 𝜒) ↔ 𝜓))
Theorem	ifpfal 1086	Value of the conditional operator for propositions when its first argument is false. Analogue for propositions of iffalse 4488. This is essentially dedlemb 1057. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 25-Jun-2020.)
⊢ (¬ 𝜑 → (if-(𝜑, 𝜓, 𝜒) ↔ 𝜒))
Theorem	ifpid 1087	Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of ifid 4520. This is essentially pm4.42 1064. (Contributed by BJ, 20-Sep-2019.)
⊢ (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓)
Theorem	casesifp 1088	Version of cases 1053 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 1085 and ifpfal 1086. (Contributed by BJ, 20-Sep-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (¬ 𝜑 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜓 ↔ if-(𝜑, 𝜒, 𝜃))
Theorem	ifpbi123d 1089	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 1090	Equivalence deduction for conditional operator for propositions. Convenience theorem for a frequent case. (Contributed by Wolf Lammen, 28-Apr-2024.)
⊢ (𝜑 → (𝜒 ↔ 𝜂))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜁))    ⇒   ⊢ (𝜑 → (if-(𝜓, 𝜒, 𝜃) ↔ if-(𝜓, 𝜂, 𝜁)))
Theorem	ifpimpda 1091	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 1092	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 4538. For more information on the weak deduction theorem, see the Weak Deduction Theorem page mmdeduction.html 4538.
Theorem	elimh 1093	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 1094	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 1095	Proof of con3 153 from its associated inference con3i 154 that illustrates the use of the weak deduction theorem dedt 1094. (Contributed by NM, 27-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) Revised dedt 1094 and elimh 1093. (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 1096	Extend wff definition to include three-way disjunction ('or').
wff (𝜑 ∨ 𝜓 ∨ 𝜒)
Syntax	w3a 1097	Extend wff definition to include three-way conjunction ('and').
wff (𝜑 ∧ 𝜓 ∧ 𝜒)
Definition	df-3or 1098	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 932. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
Definition	df-3an 1099	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 1100	Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))