P. 3 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 201-300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mpbid 201	A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ψ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → χ)
Theorem	mpbii 202	An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
⊢ ψ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → χ)
Theorem	sylibr 203	A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ψ)    &   ⊢ (χ ↔ ψ)    ⇒   ⊢ (φ → χ)
Theorem	sylbir 204	A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 5-Aug-1993.)
⊢ (ψ ↔ φ)    &   ⊢ (ψ → χ)    ⇒   ⊢ (φ → χ)
Theorem	sylibd 205	A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (χ ↔ θ))    ⇒   ⊢ (φ → (ψ → θ))
Theorem	sylbid 206	A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (χ → θ))    ⇒   ⊢ (φ → (ψ → θ))
Theorem	mpbidi 207	A deduction from a biconditional, related to modus ponens. (Contributed by NM, 9-Aug-1994.)
⊢ (θ → (φ → ψ))    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (θ → (φ → χ))
Theorem	syl5bi 208	A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ψ)    &   ⊢ (χ → (ψ → θ))    ⇒   ⊢ (χ → (φ → θ))
Theorem	syl5bir 209	A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
⊢ (ψ ↔ φ)    &   ⊢ (χ → (ψ → θ))    ⇒   ⊢ (χ → (φ → θ))
Theorem	syl5ib 210	A mixed syllogism inference. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ψ)    &   ⊢ (χ → (ψ ↔ θ))    ⇒   ⊢ (χ → (φ → θ))
Theorem	syl5ibcom 211	A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)
⊢ (φ → ψ)    &   ⊢ (χ → (ψ ↔ θ))    ⇒   ⊢ (φ → (χ → θ))
Theorem	syl5ibr 212	A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)
⊢ (φ → θ)    &   ⊢ (χ → (ψ ↔ θ))    ⇒   ⊢ (χ → (φ → ψ))
Theorem	syl5ibrcom 213	A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)
⊢ (φ → θ)    &   ⊢ (χ → (ψ ↔ θ))    ⇒   ⊢ (φ → (χ → ψ))
Theorem	biimprd 214	Deduce a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (χ → ψ))
Theorem	biimpcd 215	Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (ψ → (φ → χ))
Theorem	biimprcd 216	Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (χ → (φ → ψ))
Theorem	syl6ib 217	A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ → χ))    &   ⊢ (χ ↔ θ)    ⇒   ⊢ (φ → (ψ → θ))
Theorem	syl6ibr 218	A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ → χ))    &   ⊢ (θ ↔ χ)    ⇒   ⊢ (φ → (ψ → θ))
Theorem	syl6bi 219	A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (χ → θ)    ⇒   ⊢ (φ → (ψ → θ))
Theorem	syl6bir 220	A mixed syllogism inference. (Contributed by NM, 18-May-1994.)
⊢ (φ → (χ ↔ ψ))    &   ⊢ (χ → θ)    ⇒   ⊢ (φ → (ψ → θ))
Theorem	syl7bi 221	A mixed syllogism inference from a doubly nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ψ)    &   ⊢ (χ → (θ → (ψ → τ)))    ⇒   ⊢ (χ → (θ → (φ → τ)))
Theorem	syl8ib 222	A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 1-Aug-1994.)
⊢ (φ → (ψ → (χ → θ)))    &   ⊢ (θ ↔ τ)    ⇒   ⊢ (φ → (ψ → (χ → τ)))
Theorem	mpbird 223	A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → χ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ψ)
Theorem	mpbiri 224	An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
⊢ χ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ψ)
Theorem	sylibrd 225	A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (θ ↔ χ))    ⇒   ⊢ (φ → (ψ → θ))
Theorem	sylbird 226	A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
⊢ (φ → (χ ↔ ψ))    &   ⊢ (φ → (χ → θ))    ⇒   ⊢ (φ → (ψ → θ))
Theorem	biid 227	Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ φ)
Theorem	biidd 228	Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.)
⊢ (φ → (ψ ↔ ψ))
Theorem	pm5.1im 229	Two propositions are equivalent if they are both true. Closed form of 2th 230. Equivalent to a bi1 178-like version of the xor-connective. This theorem stays true, no matter how you permute its operands. This is evident from its sharper version (φ ↔ (ψ ↔ (φ ↔ ψ))). (Contributed by Wolf Lammen, 12-May-2013.)
⊢ (φ → (ψ → (φ ↔ ψ)))
Theorem	2th 230	Two truths are equivalent. (Contributed by NM, 18-Aug-1993.)
⊢ φ    &   ⊢ ψ    ⇒   ⊢ (φ ↔ ψ)
Theorem	2thd 231	Two truths are equivalent (deduction rule). (Contributed by NM, 3-Jun-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    ⇒   ⊢ (φ → (ψ ↔ χ))
Theorem	ibi 232	Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 17-Oct-2003.)
⊢ (φ → (φ ↔ ψ))    ⇒   ⊢ (φ → ψ)
Theorem	ibir 233	Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.)
⊢ (φ → (ψ ↔ φ))    ⇒   ⊢ (φ → ψ)
Theorem	ibd 234	Deduction that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 26-Jun-2004.)
⊢ (φ → (ψ → (ψ ↔ χ)))    ⇒   ⊢ (φ → (ψ → χ))
Theorem	pm5.74 235	Distribution of implication over biconditional. Theorem *5.74 of [WhiteheadRussell] p. 126. (Contributed by NM, 1-Aug-1994.) (Proof shortened by Wolf Lammen, 11-Apr-2013.)
⊢ ((φ → (ψ ↔ χ)) ↔ ((φ → ψ) ↔ (φ → χ)))
Theorem	pm5.74i 236	Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ ((φ → ψ) ↔ (φ → χ))
Theorem	pm5.74ri 237	Distribution of implication over biconditional (reverse inference rule). (Contributed by NM, 1-Aug-1994.)
⊢ ((φ → ψ) ↔ (φ → χ))    ⇒   ⊢ (φ → (ψ ↔ χ))
Theorem	pm5.74d 238	Distribution of implication over biconditional (deduction rule). (Contributed by NM, 21-Mar-1996.)
⊢ (φ → (ψ → (χ ↔ θ)))    ⇒   ⊢ (φ → ((ψ → χ) ↔ (ψ → θ)))
Theorem	pm5.74rd 239	Distribution of implication over biconditional (deduction rule). (Contributed by NM, 19-Mar-1997.)
⊢ (φ → ((ψ → χ) ↔ (ψ → θ)))    ⇒   ⊢ (φ → (ψ → (χ ↔ θ)))
Theorem	bitri 240	An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)
⊢ (φ ↔ ψ)    &   ⊢ (ψ ↔ χ)    ⇒   ⊢ (φ ↔ χ)
Theorem	bitr2i 241	An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ψ)    &   ⊢ (ψ ↔ χ)    ⇒   ⊢ (χ ↔ φ)
Theorem	bitr3i 242	An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (ψ ↔ φ)    &   ⊢ (ψ ↔ χ)    ⇒   ⊢ (φ ↔ χ)
Theorem	bitr4i 243	An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ψ)    &   ⊢ (χ ↔ ψ)    ⇒   ⊢ (φ ↔ χ)
Theorem	bitrd 244	Deduction form of bitri 240. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (χ ↔ θ))    ⇒   ⊢ (φ → (ψ ↔ θ))
Theorem	bitr2d 245	Deduction form of bitr2i 241. (Contributed by NM, 9-Jun-2004.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (χ ↔ θ))    ⇒   ⊢ (φ → (θ ↔ ψ))
Theorem	bitr3d 246	Deduction form of bitr3i 242. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (ψ ↔ θ))    ⇒   ⊢ (φ → (χ ↔ θ))
Theorem	bitr4d 247	Deduction form of bitr4i 243. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ χ))    ⇒   ⊢ (φ → (ψ ↔ θ))
Theorem	syl5bb 248	A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ψ)    &   ⊢ (χ → (ψ ↔ θ))    ⇒   ⊢ (χ → (φ ↔ θ))
Theorem	syl5rbb 249	A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ψ)    &   ⊢ (χ → (ψ ↔ θ))    ⇒   ⊢ (χ → (θ ↔ φ))
Theorem	syl5bbr 250	A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
⊢ (ψ ↔ φ)    &   ⊢ (χ → (ψ ↔ θ))    ⇒   ⊢ (χ → (φ ↔ θ))
Theorem	syl5rbbr 251	A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
⊢ (ψ ↔ φ)    &   ⊢ (χ → (ψ ↔ θ))    ⇒   ⊢ (χ → (θ ↔ φ))
Theorem	syl6bb 252	A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (χ ↔ θ)    ⇒   ⊢ (φ → (ψ ↔ θ))
Theorem	syl6rbb 253	A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (χ ↔ θ)    ⇒   ⊢ (φ → (θ ↔ ψ))
Theorem	syl6bbr 254	A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ ↔ χ)    ⇒   ⊢ (φ → (ψ ↔ θ))
Theorem	syl6rbbr 255	A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ ↔ χ)    ⇒   ⊢ (φ → (θ ↔ ψ))
Theorem	3imtr3i 256	A mixed syllogism inference, useful for removing a definition from both sides of an implication. (Contributed by NM, 10-Aug-1994.)
⊢ (φ → ψ)    &   ⊢ (φ ↔ χ)    &   ⊢ (ψ ↔ θ)    ⇒   ⊢ (χ → θ)
Theorem	3imtr4i 257	A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ψ)    &   ⊢ (χ ↔ φ)    &   ⊢ (θ ↔ ψ)    ⇒   ⊢ (χ → θ)
Theorem	3imtr3d 258	More general version of 3imtr3i 256. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (ψ ↔ θ))    &   ⊢ (φ → (χ ↔ τ))    ⇒   ⊢ (φ → (θ → τ))
Theorem	3imtr4d 259	More general version of 3imtr4i 257. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (θ ↔ ψ))    &   ⊢ (φ → (τ ↔ χ))    ⇒   ⊢ (φ → (θ → τ))
Theorem	3imtr3g 260	More general version of 3imtr3i 256. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
⊢ (φ → (ψ → χ))    &   ⊢ (ψ ↔ θ)    &   ⊢ (χ ↔ τ)    ⇒   ⊢ (φ → (θ → τ))
Theorem	3imtr4g 261	More general version of 3imtr4i 257. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
⊢ (φ → (ψ → χ))    &   ⊢ (θ ↔ ψ)    &   ⊢ (τ ↔ χ)    ⇒   ⊢ (φ → (θ → τ))
Theorem	3bitri 262	A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ψ)    &   ⊢ (ψ ↔ χ)    &   ⊢ (χ ↔ θ)    ⇒   ⊢ (φ ↔ θ)
Theorem	3bitrri 263	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
⊢ (φ ↔ ψ)    &   ⊢ (ψ ↔ χ)    &   ⊢ (χ ↔ θ)    ⇒   ⊢ (θ ↔ φ)
Theorem	3bitr2i 264	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
⊢ (φ ↔ ψ)    &   ⊢ (χ ↔ ψ)    &   ⊢ (χ ↔ θ)    ⇒   ⊢ (φ ↔ θ)
Theorem	3bitr2ri 265	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
⊢ (φ ↔ ψ)    &   ⊢ (χ ↔ ψ)    &   ⊢ (χ ↔ θ)    ⇒   ⊢ (θ ↔ φ)
Theorem	3bitr3i 266	A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.)
⊢ (φ ↔ ψ)    &   ⊢ (φ ↔ χ)    &   ⊢ (ψ ↔ θ)    ⇒   ⊢ (χ ↔ θ)
Theorem	3bitr3ri 267	A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ψ)    &   ⊢ (φ ↔ χ)    &   ⊢ (ψ ↔ θ)    ⇒   ⊢ (θ ↔ χ)
Theorem	3bitr4i 268	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, 5-Aug-1993.)
⊢ (φ ↔ ψ)    &   ⊢ (χ ↔ φ)    &   ⊢ (θ ↔ ψ)    ⇒   ⊢ (χ ↔ θ)
Theorem	3bitr4ri 269	A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)
⊢ (φ ↔ ψ)    &   ⊢ (χ ↔ φ)    &   ⊢ (θ ↔ ψ)    ⇒   ⊢ (θ ↔ χ)
Theorem	3bitrd 270	Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (χ ↔ θ))    &   ⊢ (φ → (θ ↔ τ))    ⇒   ⊢ (φ → (ψ ↔ τ))
Theorem	3bitrrd 271	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (χ ↔ θ))    &   ⊢ (φ → (θ ↔ τ))    ⇒   ⊢ (φ → (τ ↔ ψ))
Theorem	3bitr2d 272	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ χ))    &   ⊢ (φ → (θ ↔ τ))    ⇒   ⊢ (φ → (ψ ↔ τ))
Theorem	3bitr2rd 273	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ χ))    &   ⊢ (φ → (θ ↔ τ))    ⇒   ⊢ (φ → (τ ↔ ψ))
Theorem	3bitr3d 274	Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (ψ ↔ θ))    &   ⊢ (φ → (χ ↔ τ))    ⇒   ⊢ (φ → (θ ↔ τ))
Theorem	3bitr3rd 275	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (ψ ↔ θ))    &   ⊢ (φ → (χ ↔ τ))    ⇒   ⊢ (φ → (τ ↔ θ))
Theorem	3bitr4d 276	Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ ψ))    &   ⊢ (φ → (τ ↔ χ))    ⇒   ⊢ (φ → (θ ↔ τ))
Theorem	3bitr4rd 277	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ ψ))    &   ⊢ (φ → (τ ↔ χ))    ⇒   ⊢ (φ → (τ ↔ θ))
Theorem	3bitr3g 278	More general version of 3bitr3i 266. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (ψ ↔ θ)    &   ⊢ (χ ↔ τ)    ⇒   ⊢ (φ → (θ ↔ τ))
Theorem	3bitr4g 279	More general version of 3bitr4i 268. Useful for converting definitions in a formula. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ ↔ ψ)    &   ⊢ (τ ↔ χ)    ⇒   ⊢ (φ → (θ ↔ τ))
Theorem	bi3ant 280	Construct a bi-conditional in antecedent position. (Contributed by Wolf Lammen, 14-May-2013.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (((θ → τ) → φ) → (((τ → θ) → ψ) → ((θ ↔ τ) → χ)))
Theorem	bisym 281	Express symmetries of theorems in terms of biconditionals. (Contributed by Wolf Lammen, 14-May-2013.)
⊢ (((φ → ψ) → (χ → θ)) → (((ψ → φ) → (θ → χ)) → ((φ ↔ ψ) → (χ ↔ θ))))
Theorem	notnot 282	Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ¬ ¬ φ)
Theorem	con34b 283	Contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116. (Contributed by NM, 5-Aug-1993.)
⊢ ((φ → ψ) ↔ (¬ ψ → ¬ φ))
Theorem	con4bid 284	A contraposition deduction. (Contributed by NM, 21-May-1994.)
⊢ (φ → (¬ ψ ↔ ¬ χ))    ⇒   ⊢ (φ → (ψ ↔ χ))
Theorem	notbid 285	Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (¬ ψ ↔ ¬ χ))
Theorem	notbi 286	Contraposition. Theorem *4.11 of [WhiteheadRussell] p. 117. (Contributed by NM, 21-May-1994.) (Proof shortened by Wolf Lammen, 12-Jun-2013.)
⊢ ((φ ↔ ψ) ↔ (¬ φ ↔ ¬ ψ))
Theorem	notbii 287	Negate both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (¬ φ ↔ ¬ ψ)
Theorem	con4bii 288	A contraposition inference. (Contributed by NM, 21-May-1994.)
⊢ (¬ φ ↔ ¬ ψ)    ⇒   ⊢ (φ ↔ ψ)
Theorem	mtbi 289	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 290	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 291	A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)
⊢ (φ → ¬ ψ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ¬ χ)
Theorem	mtbird 292	A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.)
⊢ (φ → ¬ χ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	mtbii 293	An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.)
⊢ ¬ ψ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ¬ χ)
Theorem	mtbiri 294	An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.)
⊢ ¬ χ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	sylnib 295	A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)
⊢ (φ → ¬ ψ)    &   ⊢ (ψ ↔ χ)    ⇒   ⊢ (φ → ¬ χ)
Theorem	sylnibr 296	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 297	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 298	A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.)
⊢ (ψ ↔ φ)    &   ⊢ (¬ ψ → χ)    ⇒   ⊢ (¬ φ → χ)
Theorem	xchnxbi 299	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
⊢ (¬ φ ↔ ψ)    &   ⊢ (φ ↔ χ)    ⇒   ⊢ (¬ χ ↔ ψ)
Theorem	xchnxbir 300	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
⊢ (¬ φ ↔ ψ)    &   ⊢ (χ ↔ φ)    ⇒   ⊢ (¬ χ ↔ ψ)