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 45422. (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	biluk 389	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 390	Theorem *5.19 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.)
⊢ ¬ (𝜑 ↔ ¬ 𝜑)
Theorem	bi2.04 391	Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 11-May-1993.)
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))
Theorem	pm5.4 392	Antecedent absorption implication. Theorem *5.4 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.)
⊢ ((𝜑 → (𝜑 → 𝜓)) ↔ (𝜑 → 𝜓))
Theorem	imdi 393	Distributive law for implication. Compare Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.)
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	pm5.41 394	Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 12-Oct-2012.)
⊢ (((𝜑 → 𝜓) → (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 → 𝜒)))
Theorem	imbibi 395	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 396	Obsolete version of imbibi 395 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 397	Theorem *4.8 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → ¬ 𝜑) ↔ ¬ 𝜑)
Theorem	pm4.81 398	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 399	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.)
⊢ ((𝜓 → 𝜑) → (((𝜑 → 𝜒) → (𝜓 → 𝜃)) ↔ (𝜓 → (𝜒 → 𝜃))))
1.2.6  Logical conjunction This section defines conjunction of two formulas, denoted by infix "∧ " and read "and". It is defined in terms of implication and negation, which is possible in classical logic (but not in intuitionistic logic: see iset.mm). After the definition, we briefly introduce conversion of simple expressions to and from conjunction. Two simple operations called importation (imp 411) and exportation (ex 417) follow. In the propositions-as-types interpretation, they correspond to uncurrying and currying respectively. They are foundational for this section. Most of the theorems proved here trace back to them, mostly indirectly, in a layered fashion, where more complex expressions are built from simpler ones. Here are some of these successive layers: importation and exportation, commutativity and associativity laws, adding antecedents and simplifying, conjunction of consequents, syllogisms, etc. As indicated in the "note on definitions" in the section comment for logical equivalence, some theorems containing only implication, negation and conjunction are placed in the section after disjunction since theirs proofs use disjunction (although this is not required since definitions are conservative, see said section comment).
Syntax	wa 400	Extend wff definition to include conjunction ("and").
wff (𝜑 ∧ 𝜓)