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.)
|- (ph -> ps)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> ch)
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.)
|- ps   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> ch)
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.)
|- (ph -> ps)   &   |- (ch <-> ps)   =>   |- (ph -> ch)
Theorem	sylbir 204	A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 5-Aug-1993.)
|- (ps <-> ph)   &   |- (ps -> ch)   =>   |- (ph -> ch)
Theorem	sylibd 205	A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
|- (ph -> (ps -> ch))   &   |- (ph -> (ch <-> th))   =>   |- (ph -> (ps -> th))
Theorem	sylbid 206	A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (ch -> th))   =>   |- (ph -> (ps -> th))
Theorem	mpbidi 207	A deduction from a biconditional, related to modus ponens. (Contributed by NM, 9-Aug-1994.)
|- (th -> (ph -> ps))   &   |- (ph -> (ps <-> ch))   =>   |- (th -> (ph -> ch))
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.)
|- (ph <-> ps)   &   |- (ch -> (ps -> th))   =>   |- (ch -> (ph -> th))
Theorem	syl5bir 209	A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
|- (ps <-> ph)   &   |- (ch -> (ps -> th))   =>   |- (ch -> (ph -> th))
Theorem	syl5ib 210	A mixed syllogism inference. (Contributed by NM, 5-Aug-1993.)
|- (ph -> ps)   &   |- (ch -> (ps <-> th))   =>   |- (ch -> (ph -> th))
Theorem	syl5ibcom 211	A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)
|- (ph -> ps)   &   |- (ch -> (ps <-> th))   =>   |- (ph -> (ch -> th))
Theorem	syl5ibr 212	A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)
|- (ph -> th)   &   |- (ch -> (ps <-> th))   =>   |- (ch -> (ph -> ps))
Theorem	syl5ibrcom 213	A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)
|- (ph -> th)   &   |- (ch -> (ps <-> th))   =>   |- (ph -> (ch -> ps))
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.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> (ch -> ps))
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.)
|- (ph -> (ps <-> ch))   =>   |- (ps -> (ph -> ch))
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.)
|- (ph -> (ps <-> ch))   =>   |- (ch -> (ph -> ps))
Theorem	syl6ib 217	A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps -> ch))   &   |- (ch <-> th)   =>   |- (ph -> (ps -> th))
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.)
|- (ph -> (ps -> ch))   &   |- (th <-> ch)   =>   |- (ph -> (ps -> th))
Theorem	syl6bi 219	A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)
|- (ph -> (ps <-> ch))   &   |- (ch -> th)   =>   |- (ph -> (ps -> th))
Theorem	syl6bir 220	A mixed syllogism inference. (Contributed by NM, 18-May-1994.)
|- (ph -> (ch <-> ps))   &   |- (ch -> th)   =>   |- (ph -> (ps -> th))
Theorem	syl7bi 221	A mixed syllogism inference from a doubly nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
|- (ph <-> ps)   &   |- (ch -> (th -> (ps -> ta)))   =>   |- (ch -> (th -> (ph -> ta)))
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.)
|- (ph -> (ps -> (ch -> th)))   &   |- (th <-> ta)   =>   |- (ph -> (ps -> (ch -> ta)))
Theorem	mpbird 223	A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
|- (ph -> ch)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> ps)
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.)
|- ch   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> ps)
Theorem	sylibrd 225	A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
|- (ph -> (ps -> ch))   &   |- (ph -> (th <-> ch))   =>   |- (ph -> (ps -> th))
Theorem	sylbird 226	A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
|- (ph -> (ch <-> ps))   &   |- (ph -> (ch -> th))   =>   |- (ph -> (ps -> th))
Theorem	biid 227	Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.)
|- (ph <-> ph)
Theorem	biidd 228	Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.)
|- (ph -> (ps <-> ps))
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 (ph <-> (ps <-> (ph <-> ps))). (Contributed by Wolf Lammen, 12-May-2013.)
|- (ph -> (ps -> (ph <-> ps)))
Theorem	2th 230	Two truths are equivalent. (Contributed by NM, 18-Aug-1993.)
|- ph   &   |- ps   =>   |- (ph <-> ps)
Theorem	2thd 231	Two truths are equivalent (deduction rule). (Contributed by NM, 3-Jun-2012.)
|- (ph -> ps)   &   |- (ph -> ch)   =>   |- (ph -> (ps <-> ch))
Theorem	ibi 232	Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 17-Oct-2003.)
|- (ph -> (ph <-> ps))   =>   |- (ph -> ps)
Theorem	ibir 233	Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.)
|- (ph -> (ps <-> ph))   =>   |- (ph -> ps)
Theorem	ibd 234	Deduction that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 26-Jun-2004.)
|- (ph -> (ps -> (ps <-> ch)))   =>   |- (ph -> (ps -> ch))
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.)
|- ((ph -> (ps <-> ch)) <-> ((ph -> ps) <-> (ph -> ch)))
Theorem	pm5.74i 236	Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.)
|- (ph -> (ps <-> ch))   =>   |- ((ph -> ps) <-> (ph -> ch))
Theorem	pm5.74ri 237	Distribution of implication over biconditional (reverse inference rule). (Contributed by NM, 1-Aug-1994.)
|- ((ph -> ps) <-> (ph -> ch))   =>   |- (ph -> (ps <-> ch))
Theorem	pm5.74d 238	Distribution of implication over biconditional (deduction rule). (Contributed by NM, 21-Mar-1996.)
|- (ph -> (ps -> (ch <-> th)))   =>   |- (ph -> ((ps -> ch) <-> (ps -> th)))
Theorem	pm5.74rd 239	Distribution of implication over biconditional (deduction rule). (Contributed by NM, 19-Mar-1997.)
|- (ph -> ((ps -> ch) <-> (ps -> th)))   =>   |- (ph -> (ps -> (ch <-> th)))
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.)
|- (ph <-> ps)   &   |- (ps <-> ch)   =>   |- (ph <-> ch)
Theorem	bitr2i 241	An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
|- (ph <-> ps)   &   |- (ps <-> ch)   =>   |- (ch <-> ph)
Theorem	bitr3i 242	An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
|- (ps <-> ph)   &   |- (ps <-> ch)   =>   |- (ph <-> ch)
Theorem	bitr4i 243	An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
|- (ph <-> ps)   &   |- (ch <-> ps)   =>   |- (ph <-> ch)
Theorem	bitrd 244	Deduction form of bitri 240. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (ch <-> th))   =>   |- (ph -> (ps <-> th))
Theorem	bitr2d 245	Deduction form of bitr2i 241. (Contributed by NM, 9-Jun-2004.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (ch <-> th))   =>   |- (ph -> (th <-> ps))
Theorem	bitr3d 246	Deduction form of bitr3i 242. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (ps <-> th))   =>   |- (ph -> (ch <-> th))
Theorem	bitr4d 247	Deduction form of bitr4i 243. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ch))   =>   |- (ph -> (ps <-> th))
Theorem	syl5bb 248	A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
|- (ph <-> ps)   &   |- (ch -> (ps <-> th))   =>   |- (ch -> (ph <-> th))
Theorem	syl5rbb 249	A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
|- (ph <-> ps)   &   |- (ch -> (ps <-> th))   =>   |- (ch -> (th <-> ph))
Theorem	syl5bbr 250	A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
|- (ps <-> ph)   &   |- (ch -> (ps <-> th))   =>   |- (ch -> (ph <-> th))
Theorem	syl5rbbr 251	A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
|- (ps <-> ph)   &   |- (ch -> (ps <-> th))   =>   |- (ch -> (th <-> ph))
Theorem	syl6bb 252	A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps <-> ch))   &   |- (ch <-> th)   =>   |- (ph -> (ps <-> th))
Theorem	syl6rbb 253	A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps <-> ch))   &   |- (ch <-> th)   =>   |- (ph -> (th <-> ps))
Theorem	syl6bbr 254	A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps <-> ch))   &   |- (th <-> ch)   =>   |- (ph -> (ps <-> th))
Theorem	syl6rbbr 255	A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
|- (ph -> (ps <-> ch))   &   |- (th <-> ch)   =>   |- (ph -> (th <-> ps))
Theorem	3imtr3i 256	A mixed syllogism inference, useful for removing a definition from both sides of an implication. (Contributed by NM, 10-Aug-1994.)
|- (ph -> ps)   &   |- (ph <-> ch)   &   |- (ps <-> th)   =>   |- (ch -> th)
Theorem	3imtr4i 257	A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
|- (ph -> ps)   &   |- (ch <-> ph)   &   |- (th <-> ps)   =>   |- (ch -> th)
Theorem	3imtr3d 258	More general version of 3imtr3i 256. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.)
|- (ph -> (ps -> ch))   &   |- (ph -> (ps <-> th))   &   |- (ph -> (ch <-> ta))   =>   |- (ph -> (th -> ta))
Theorem	3imtr4d 259	More general version of 3imtr4i 257. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.)
|- (ph -> (ps -> ch))   &   |- (ph -> (th <-> ps))   &   |- (ph -> (ta <-> ch))   =>   |- (ph -> (th -> ta))
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.)
|- (ph -> (ps -> ch))   &   |- (ps <-> th)   &   |- (ch <-> ta)   =>   |- (ph -> (th -> ta))
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.)
|- (ph -> (ps -> ch))   &   |- (th <-> ps)   &   |- (ta <-> ch)   =>   |- (ph -> (th -> ta))
Theorem	3bitri 262	A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
|- (ph <-> ps)   &   |- (ps <-> ch)   &   |- (ch <-> th)   =>   |- (ph <-> th)
Theorem	3bitrri 263	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
|- (ph <-> ps)   &   |- (ps <-> ch)   &   |- (ch <-> th)   =>   |- (th <-> ph)
Theorem	3bitr2i 264	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
|- (ph <-> ps)   &   |- (ch <-> ps)   &   |- (ch <-> th)   =>   |- (ph <-> th)
Theorem	3bitr2ri 265	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
|- (ph <-> ps)   &   |- (ch <-> ps)   &   |- (ch <-> th)   =>   |- (th <-> ph)
Theorem	3bitr3i 266	A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.)
|- (ph <-> ps)   &   |- (ph <-> ch)   &   |- (ps <-> th)   =>   |- (ch <-> th)
Theorem	3bitr3ri 267	A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
|- (ph <-> ps)   &   |- (ph <-> ch)   &   |- (ps <-> th)   =>   |- (th <-> ch)
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.)
|- (ph <-> ps)   &   |- (ch <-> ph)   &   |- (th <-> ps)   =>   |- (ch <-> th)
Theorem	3bitr4ri 269	A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)
|- (ph <-> ps)   &   |- (ch <-> ph)   &   |- (th <-> ps)   =>   |- (th <-> ch)
Theorem	3bitrd 270	Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (ch <-> th))   &   |- (ph -> (th <-> ta))   =>   |- (ph -> (ps <-> ta))
Theorem	3bitrrd 271	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (ch <-> th))   &   |- (ph -> (th <-> ta))   =>   |- (ph -> (ta <-> ps))
Theorem	3bitr2d 272	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ch))   &   |- (ph -> (th <-> ta))   =>   |- (ph -> (ps <-> ta))
Theorem	3bitr2rd 273	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ch))   &   |- (ph -> (th <-> ta))   =>   |- (ph -> (ta <-> ps))
Theorem	3bitr3d 274	Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (ps <-> th))   &   |- (ph -> (ch <-> ta))   =>   |- (ph -> (th <-> ta))
Theorem	3bitr3rd 275	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (ps <-> th))   &   |- (ph -> (ch <-> ta))   =>   |- (ph -> (ta <-> th))
Theorem	3bitr4d 276	Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ps))   &   |- (ph -> (ta <-> ch))   =>   |- (ph -> (th <-> ta))
Theorem	3bitr4rd 277	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ps))   &   |- (ph -> (ta <-> ch))   =>   |- (ph -> (ta <-> th))
Theorem	3bitr3g 278	More general version of 3bitr3i 266. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.)
|- (ph -> (ps <-> ch))   &   |- (ps <-> th)   &   |- (ch <-> ta)   =>   |- (ph -> (th <-> ta))
Theorem	3bitr4g 279	More general version of 3bitr4i 268. Useful for converting definitions in a formula. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps <-> ch))   &   |- (th <-> ps)   &   |- (ta <-> ch)   =>   |- (ph -> (th <-> ta))
Theorem	bi3ant 280	Construct a bi-conditional in antecedent position. (Contributed by Wolf Lammen, 14-May-2013.)
|- (ph -> (ps -> ch))   =>   |- (((th -> ta) -> ph) -> (((ta -> th) -> ps) -> ((th <-> ta) -> ch)))
Theorem	bisym 281	Express symmetries of theorems in terms of biconditionals. (Contributed by Wolf Lammen, 14-May-2013.)
|- (((ph -> ps) -> (ch -> th)) -> (((ps -> ph) -> (th -> ch)) -> ((ph <-> ps) -> (ch <-> th))))
Theorem	notnot 282	Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.)
|- (ph <-> -. -. ph)
Theorem	con34b 283	Contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116. (Contributed by NM, 5-Aug-1993.)
|- ((ph -> ps) <-> (-. ps -> -. ph))
Theorem	con4bid 284	A contraposition deduction. (Contributed by NM, 21-May-1994.)
|- (ph -> (-. ps <-> -. ch))   =>   |- (ph -> (ps <-> ch))
Theorem	notbid 285	Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> (-. ps <-> -. ch))
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.)
|- ((ph <-> ps) <-> (-. ph <-> -. ps))
Theorem	notbii 287	Negate both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
|- (ph <-> ps)   =>   |- (-. ph <-> -. ps)
Theorem	con4bii 288	A contraposition inference. (Contributed by NM, 21-May-1994.)
|- (-. ph <-> -. ps)   =>   |- (ph <-> ps)
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.)
|- -. ph   &   |- (ph <-> ps)   =>   |- -. ps
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.)
|- -. ps   &   |- (ph <-> ps)   =>   |- -. ph
Theorem	mtbid 291	A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)
|- (ph -> -. ps)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ch)
Theorem	mtbird 292	A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.)
|- (ph -> -. ch)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ps)
Theorem	mtbii 293	An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.)
|- -. ps   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ch)
Theorem	mtbiri 294	An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.)
|- -. ch   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ps)
Theorem	sylnib 295	A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)
|- (ph -> -. ps)   &   |- (ps <-> ch)   =>   |- (ph -> -. ch)
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.)
|- (ph -> -. ps)   &   |- (ch <-> ps)   =>   |- (ph -> -. ch)
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.)
|- (ph <-> ps)   &   |- (-. ps -> ch)   =>   |- (-. ph -> ch)
Theorem	sylnbir 298	A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.)
|- (ps <-> ph)   &   |- (-. ps -> ch)   =>   |- (-. ph -> ch)
Theorem	xchnxbi 299	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
|- (-. ph <-> ps)   &   |- (ph <-> ch)   =>   |- (-. ch <-> ps)
Theorem	xchnxbir 300	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
|- (-. ph <-> ps)   &   |- (ch <-> ph)   =>   |- (-. ch <-> ps)