P. 4 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 301-400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	3bitrri 301	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (𝜃 ↔ 𝜑)
Theorem	3bitr2i 302	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (𝜑 ↔ 𝜃)
Theorem	3bitr2ri 303	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (𝜃 ↔ 𝜑)
Theorem	3bitr3i 304	A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜑 ↔ 𝜒)    &   ⊢ (𝜓 ↔ 𝜃)    ⇒   ⊢ (𝜒 ↔ 𝜃)
Theorem	3bitr3ri 305	A chained inference from transitive law for logical equivalence. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜑 ↔ 𝜒)    &   ⊢ (𝜓 ↔ 𝜃)    ⇒   ⊢ (𝜃 ↔ 𝜒)
Theorem	3bitr4i 306	A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜓)    ⇒   ⊢ (𝜒 ↔ 𝜃)
Theorem	3bitr4ri 307	A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜓)    ⇒   ⊢ (𝜃 ↔ 𝜒)
Theorem	3bitrd 308	Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜏))
Theorem	3bitrrd 309	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜏 ↔ 𝜓))
Theorem	3bitr2d 310	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜏))
Theorem	3bitr2rd 311	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜏 ↔ 𝜓))
Theorem	3bitr3d 312	Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜃 ↔ 𝜏))
Theorem	3bitr3rd 313	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜏 ↔ 𝜃))
Theorem	3bitr4d 314	Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜓))    &   ⊢ (𝜑 → (𝜏 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜃 ↔ 𝜏))
Theorem	3bitr4rd 315	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜓))    &   ⊢ (𝜑 → (𝜏 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜏 ↔ 𝜃))
Theorem	3bitr3g 316	More general version of 3bitr3i 304. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜓 ↔ 𝜃)    &   ⊢ (𝜒 ↔ 𝜏)    ⇒   ⊢ (𝜑 → (𝜃 ↔ 𝜏))
Theorem	3bitr4g 317	More general version of 3bitr4i 306. Useful for converting definitions in a formula. (Contributed by NM, 11-May-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜒)    ⇒   ⊢ (𝜑 → (𝜃 ↔ 𝜏))
Theorem	notnotb 318	Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 ↔ ¬ ¬ 𝜑)
Theorem	con34b 319	A biconditional form of contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116. (Contributed by NM, 11-May-1993.)
⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
Theorem	con4bid 320	A contraposition deduction. (Contributed by NM, 21-May-1994.)
⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	notbid 321	Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
Theorem	notbi 322	Contraposition. Theorem *4.11 of [WhiteheadRussell] p. 117. (Contributed by NM, 21-May-1994.) (Proof shortened by Wolf Lammen, 12-Jun-2013.)
⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
Theorem	notbii 323	Negate both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (¬ 𝜑 ↔ ¬ 𝜓)
Theorem	con4bii 324	A contraposition inference. (Contributed by NM, 21-May-1994.)
⊢ (¬ 𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	mtbi 325	An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
⊢ ¬ 𝜑    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ¬ 𝜓
Theorem	mtbir 326	An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.)
⊢ ¬ 𝜓    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ¬ 𝜑
Theorem	mtbid 327	A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	mtbird 328	A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	mtbii 329	An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.)
⊢ ¬ 𝜓    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	mtbiri 330	An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.)
⊢ ¬ 𝜒    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	sylnib 331	A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	sylnibr 332	A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	sylnbi 333	A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (¬ 𝜓 → 𝜒)    ⇒   ⊢ (¬ 𝜑 → 𝜒)
Theorem	sylnbir 334	A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ (¬ 𝜓 → 𝜒)    ⇒   ⊢ (¬ 𝜑 → 𝜒)
Theorem	xchnxbi 335	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
⊢ (¬ 𝜑 ↔ 𝜓)    &   ⊢ (𝜑 ↔ 𝜒)    ⇒   ⊢ (¬ 𝜒 ↔ 𝜓)
Theorem	xchnxbir 336	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
⊢ (¬ 𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜑)    ⇒   ⊢ (¬ 𝜒 ↔ 𝜓)
Theorem	xchbinx 337	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
⊢ (𝜑 ↔ ¬ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (𝜑 ↔ ¬ 𝜒)
Theorem	xchbinxr 338	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
⊢ (𝜑 ↔ ¬ 𝜓)    &   ⊢ (𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ ¬ 𝜒)
Theorem	imbi2i 339	Introduce an antecedent to both sides of a logical equivalence. This and the next three rules are useful for building up wff's around a definition, in order to make use of the definition. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))
Theorem	bibi2i 340	Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))
Theorem	bibi1i 341	Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 26-May-1993.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))
Theorem	bibi12i 342	The equivalence of two equivalences. (Contributed by NM, 26-May-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜃))
Theorem	imbi2d 343	Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒)))
Theorem	imbi1d 344	Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))
Theorem	bibi2d 345	Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))
Theorem	bibi1d 346	Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 11-May-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))
Theorem	imbi12d 347	Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 16-May-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))
Theorem	bibi12d 348	Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 26-May-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))
Theorem	imbi12 349	Closed form of imbi12i 353. Was automatically derived from its "Virtual Deduction" version and the Metamath program "MM-PA> MINIMIZE_WITH *" command. (Contributed by Alan Sare, 18-Mar-2012.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))))
Theorem	imbi1 350	Theorem *4.84 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
Theorem	imbi2 351	Theorem *4.85 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)))
Theorem	imbi1i 352	Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))
Theorem	imbi12i 353	Join two logical equivalences to form equivalence of implications. (Contributed by NM, 1-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))
Theorem	bibi1 354	Theorem *4.86 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒)))
Theorem	bitr3 355	Closed nested implication form of bitr3i 280. Derived automatically from bitr3VD 45673. (Contributed by Alan Sare, 31-Dec-2011.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) → (𝜓 ↔ 𝜒)))
Theorem	con2bi 356	Contraposition. Theorem *4.12 of [WhiteheadRussell] p. 117. (Contributed by NM, 15-Apr-1995.) (Proof shortened by Wolf Lammen, 3-Jan-2013.)
⊢ ((𝜑 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜑))
Theorem	con2bid 357	A contraposition deduction. (Contributed by NM, 15-Apr-1995.)
⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))
Theorem	con1bid 358	A contraposition deduction. (Contributed by NM, 9-Oct-1999.)
⊢ (𝜑 → (¬ 𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (¬ 𝜒 ↔ 𝜓))
Theorem	con1bii 359	A contraposition inference. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)
⊢ (¬ 𝜑 ↔ 𝜓)    ⇒   ⊢ (¬ 𝜓 ↔ 𝜑)
Theorem	con2bii 360	A contraposition inference. (Contributed by NM, 12-Mar-1993.)
⊢ (𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (𝜓 ↔ ¬ 𝜑)
Theorem	con1b 361	Contraposition. Bidirectional version of con1 147. (Contributed by NM, 3-Jan-1993.)
⊢ ((¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → 𝜑))
Theorem	con2b 362	Contraposition. Bidirectional version of con2 136. (Contributed by NM, 12-Mar-1993.)
⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑))
Theorem	biimt 363	A wff is equivalent to itself with true antecedent. (Contributed by NM, 28-Jan-1996.)
⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))
Theorem	pm5.5 364	Theorem *5.5 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓))
Theorem	a1bi 365	Inference introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜑 → 𝜓))
Theorem	mt2bi 366	A false consequent falsifies an antecedent. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜓 ↔ (𝜓 → ¬ 𝜑))
Theorem	mtt 367	Modus-tollens-like theorem. (Contributed by NM, 7-Apr-2001.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)
⊢ (¬ 𝜑 → (¬ 𝜓 ↔ (𝜓 → 𝜑)))
Theorem	imnot 368	If a proposition is false, then implying it is equivalent to being false. One of four theorems that can be used to simplify an implication (𝜑 → 𝜓), the other ones being ax-1 6 (true consequent), pm2.21 124 (false antecedent), pm5.5 364 (true antecedent). (Contributed by Mario Carneiro, 26-Apr-2019.) (Proof shortened by Wolf Lammen, 26-May-2019.)
⊢ (¬ 𝜓 → ((𝜑 → 𝜓) ↔ ¬ 𝜑))
Theorem	pm5.501 369	Theorem *5.501 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 → (𝜓 ↔ (𝜑 ↔ 𝜓)))
Theorem	ibib 370	Implication in terms of implication and biconditional. (Contributed by NM, 31-Mar-1994.) (Proof shortened by Wolf Lammen, 24-Jan-2013.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜑 ↔ 𝜓)))
Theorem	ibibr 371	Implication in terms of implication and biconditional. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 21-Dec-2013.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜓 ↔ 𝜑)))
Theorem	tbt 372	A wff is equivalent to its equivalence with a truth. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜓 ↔ 𝜑))
Theorem	nbn2 373	The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by Juha Arpiainen, 19-Jan-2006.) (Proof shortened by Wolf Lammen, 28-Jan-2013.)
⊢ (¬ 𝜑 → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓)))
Theorem	bibif 374	Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007.) (Proof shortened by Wolf Lammen, 28-Jan-2013.)
⊢ (¬ 𝜓 → ((𝜑 ↔ 𝜓) ↔ ¬ 𝜑))
Theorem	nbn 375	The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ ¬ 𝜑    ⇒   ⊢ (¬ 𝜓 ↔ (𝜓 ↔ 𝜑))
Theorem	nbn3 376	Transfer falsehood via equivalence. (Contributed by NM, 11-Sep-2006.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜓 ↔ (𝜓 ↔ ¬ 𝜑))
Theorem	pm5.21im 377	Two propositions are equivalent if they are both false. Closed form of 2false 378. Equivalent to a biimpr 223-like version of the xor-connective. (Contributed by Wolf Lammen, 13-May-2013.)
⊢ (¬ 𝜑 → (¬ 𝜓 → (𝜑 ↔ 𝜓)))
Theorem	2false 378	Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.)
⊢ ¬ 𝜑    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	2falsed 379	Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013.) (Proof shortened by Wolf Lammen, 11-Apr-2024.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	pm5.21ni 380	Two propositions implying a false one are equivalent. (Contributed by NM, 16-Feb-1996.) (Proof shortened by Wolf Lammen, 19-May-2013.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒))
Theorem	pm5.21nii 381	Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜓)    &   ⊢ (𝜓 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (𝜑 ↔ 𝜒)
Theorem	pm5.21ndd 382	Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Proof shortened by Wolf Lammen, 6-Oct-2013.)
⊢ (𝜑 → (𝜒 → 𝜓))    &   ⊢ (𝜑 → (𝜃 → 𝜓))    &   ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜒 ↔ 𝜃))
Theorem	bija 383	Combine antecedents into a single biconditional. This inference, reminiscent of ja 188, is reversible: The hypotheses can be deduced from the conclusion alone (see pm5.1im 266 and pm5.21im 377). (Contributed by Wolf Lammen, 13-May-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ↔ 𝜓) → 𝜒)
Theorem	pm5.18 384	Theorem *5.18 of [WhiteheadRussell] p. 124. This theorem says that logical equivalence is the same as negated "exclusive or". (Contributed by NM, 28-Jun-2002.) (Proof shortened by Andrew Salmon, 20-Jun-2011.) (Proof shortened by Wolf Lammen, 15-Oct-2013.)
⊢ ((𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ↔ ¬ 𝜓))
Theorem	xor3 385	Two ways to express "exclusive or". (Contributed by NM, 1-Jan-2006.)
⊢ (¬ (𝜑 ↔ 𝜓) ↔ (𝜑 ↔ ¬ 𝜓))
Theorem	nbbn 386	Move negation outside of biconditional. Compare Theorem *5.18 of [WhiteheadRussell] p. 124. (Contributed by NM, 27-Jun-2002.) (Proof shortened by Wolf Lammen, 20-Sep-2013.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ ((¬ 𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))
Theorem	nbbnOLD 387	Obsolete version of nbbn 386 as of 10-Jun-2026. (Contributed by NM, 27-Jun-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))
Theorem	biass 388	Associative law for the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs", Annals of Pure and Applied Logic, 113:207-224, 2002, http://www.cs.utexas.edu/users/ai-lab/pub-view.php?PubID=26805. Interestingly, this law was not included in Principia Mathematica but was apparently first noted by Jan Lukasiewicz circa 1923. (Contributed by NM, 8-Jan-2005.) (Proof shortened by Juha Arpiainen, 19-Jan-2006.) (Proof shortened by Wolf Lammen, 21-Sep-2013.)
⊢ (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒)))
Theorem	birot 389	Rotation of the arguments of the nested implication (. ↔ (. ↔ .)) (a general phenomenon for a commutative associative binary operation, see e.g., inrot 4181) . (Contributed by BJ, 10-Aug-2026.)
⊢ ((𝜑 ↔ (𝜓 ↔ 𝜒)) ↔ (𝜓 ↔ (𝜒 ↔ 𝜑)))
Theorem	biluk 390	Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall, ed., Polish Logic 1920-1939 (Oxford, 1967), p. 96. (Contributed by NM, 10-Jan-2005.)
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒)))
Theorem	pm5.19 391	Theorem *5.19 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.)
⊢ ¬ (𝜑 ↔ ¬ 𝜑)
Theorem	bi2.04 392	Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 11-May-1993.)
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))
Theorem	pm5.4 393	Antecedent absorption implication. Theorem *5.4 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.)
⊢ ((𝜑 → (𝜑 → 𝜓)) ↔ (𝜑 → 𝜓))
Theorem	imdi 394	Distributive law for implication. Compare Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.)
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	pm5.41 395	Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 12-Oct-2012.)
⊢ (((𝜑 → 𝜓) → (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 → 𝜒)))
Theorem	imbibi 396	The antecedent of one side of a biconditional can be moved out of the biconditional to become the antecedent of the remaining biconditional. (Contributed by BJ, 1-Jan-2025.) (Proof shortened by Wolf Lammen, 5-Jan-2025.) (Proof shortened by Garrett Katz, 15-Jun-2026.)
⊢ (((𝜑 → 𝜓) ↔ 𝜒) → (𝜑 → (𝜓 ↔ 𝜒)))
Theorem	imbibiOLD 397	Obsolete version of imbibi 396 as of 15-Jun-2026. The antecedent of one side of a biconditional can be moved out of the biconditional to become the antecedent of the remaining biconditional. (Contributed by BJ, 1-Jan-2025.) (Proof shortened by Wolf Lammen, 5-Jan-2025.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (((𝜑 → 𝜓) ↔ 𝜒) → (𝜑 → (𝜓 ↔ 𝜒)))
Theorem	pm4.8 398	Theorem *4.8 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → ¬ 𝜑) ↔ ¬ 𝜑)
Theorem	pm4.81 399	A formula is equivalent to its negation implying it. Theorem *4.81 of [WhiteheadRussell] p. 122. Note that the second step, using pm2.24 125, could also use ax-1 6. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 → 𝜑) ↔ 𝜑)
Theorem	imim21b 400	Simplify an implication between two implications when the antecedent of the first is a consequence of the antecedent of the second. The reverse form is useful in producing the successor step in induction proofs. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Wolf Lammen, 14-Sep-2013.)
⊢ ((𝜓 → 𝜑) → (((𝜑 → 𝜒) → (𝜓 → 𝜃)) ↔ (𝜓 → (𝜒 → 𝜃))))