P. 3 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 201-300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	3imtr4d 201	More general version of 3imtr4i 199. 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 202	More general version of 3imtr3i 198. 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 203	More general version of 3imtr4i 199. 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 204	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 205	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 206	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 207	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 208	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 209	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 210	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 211	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 212	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 213	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 214	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 215	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 216	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 217	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 218	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 219	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 220	More general version of 3bitr3i 208. 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 221	More general version of 3bitr4i 210. 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 222	Construct a biconditional in antecedent position. (Contributed by Wolf Lammen, 14-May-2013.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ( ( th -> ta ) -> ph ) -> ( ( ( ta -> th ) -> ps ) -> ( ( th <-> ta ) -> ch ) ) )
Theorem	bisym 223	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	imbi2i 224	Introduce an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.)
|- ( ph <-> ps )   =>    |- ( ( ch -> ph ) <-> ( ch -> ps ) )
Theorem	bibi2i 225	Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.)
|- ( ph <-> ps )   =>    |- ( ( ch <-> ph ) <-> ( ch <-> ps ) )
Theorem	bibi1i 226	Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> ps )   =>    |- ( ( ph <-> ch ) <-> ( ps <-> ch ) )
Theorem	bibi12i 227	The equivalence of two equivalences. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   =>    |- ( ( ph <-> ch ) <-> ( ps <-> th ) )
Theorem	imbi2d 228	Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( th -> ps ) <-> ( th -> ch ) ) )
Theorem	imbi1d 229	Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( ps -> th ) <-> ( ch -> th ) ) )
Theorem	bibi2d 230	Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )
Theorem	bibi1d 231	Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )
Theorem	imbi12d 232	Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   =>    |- ( ph -> ( ( ps -> th ) <-> ( ch -> ta ) ) )
Theorem	bibi12d 233	Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   =>    |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> ta ) ) )
Theorem	imbi1 234	Theorem *4.84 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph <-> ps ) -> ( ( ph -> ch ) <-> ( ps -> ch ) ) )
Theorem	imbi2 235	Theorem *4.85 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.)
|- ( ( ph <-> ps ) -> ( ( ch -> ph ) <-> ( ch -> ps ) ) )
Theorem	imbi1i 236	Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
|- ( ph <-> ps )   =>    |- ( ( ph -> ch ) <-> ( ps -> ch ) )
Theorem	imbi12i 237	Join two logical equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   =>    |- ( ( ph -> ch ) <-> ( ps -> th ) )
Theorem	bibi1 238	Theorem *4.86 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph <-> ps ) -> ( ( ph <-> ch ) <-> ( ps <-> ch ) ) )
Theorem	biimt 239	A wff is equivalent to itself with true antecedent. (Contributed by NM, 28-Jan-1996.)
|- ( ph -> ( ps <-> ( ph -> ps ) ) )
Theorem	pm5.5 240	Theorem *5.5 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ph -> ( ( ph -> ps ) <-> ps ) )
Theorem	a1bi 241	Inference rule introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
|- ph   =>    |- ( ps <-> ( ph -> ps ) )
Theorem	pm5.501 242	Theorem *5.501 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 24-Jan-2013.)
|- ( ph -> ( ps <-> ( ph <-> ps ) ) )
Theorem	ibib 243	Implication in terms of implication and biconditional. (Contributed by NM, 31-Mar-1994.) (Proof shortened by Wolf Lammen, 24-Jan-2013.)
|- ( ( ph -> ps ) <-> ( ph -> ( ph <-> ps ) ) )
Theorem	ibibr 244	Implication in terms of implication and biconditional. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 21-Dec-2013.)
|- ( ( ph -> ps ) <-> ( ph -> ( ps <-> ph ) ) )
Theorem	tbt 245	A wff is equivalent to its equivalence with truth. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ph   =>    |- ( ps <-> ( ps <-> ph ) )
Theorem	bi2.04 246	Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.)
|- ( ( ph -> ( ps -> ch ) ) <-> ( ps -> ( ph -> ch ) ) )
Theorem	pm5.4 247	Antecedent absorption implication. Theorem *5.4 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.)
|- ( ( ph -> ( ph -> ps ) ) <-> ( ph -> ps ) )
Theorem	imdi 248	Distributive law for implication. Compare Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.)
|- ( ( ph -> ( ps -> ch ) ) <-> ( ( ph -> ps ) -> ( ph -> ch ) ) )
Theorem	pm5.41 249	Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 12-Oct-2012.)
|- ( ( ( ph -> ps ) -> ( ph -> ch ) ) <-> ( ph -> ( ps -> ch ) ) )
Theorem	imim21b 250	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.)
|- ( ( ps -> ph ) -> ( ( ( ph -> ch ) -> ( ps -> th ) ) <-> ( ps -> ( ch -> th ) ) ) )
Theorem	impd 251	Importation deduction. (Contributed by NM, 31-Mar-1994.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ph -> ( ( ps /\ ch ) -> th ) )
Theorem	imp31 252	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> th )
Theorem	imp32 253	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> th )
Theorem	expd 254	Exportation deduction. (Contributed by NM, 20-Aug-1993.)
|- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ph -> ( ps -> ( ch -> th ) ) )
Theorem	expdimp 255	A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)
|- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ( ph /\ ps ) -> ( ch -> th ) )
Theorem	impancom 256	Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)
|- ( ( ph /\ ps ) -> ( ch -> th ) )   =>    |- ( ( ph /\ ch ) -> ( ps -> th ) )
Theorem	pm3.3 257	Theorem *3.3 (Exp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
|- ( ( ( ph /\ ps ) -> ch ) -> ( ph -> ( ps -> ch ) ) )
Theorem	pm3.31 258	Theorem *3.31 (Imp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ( ph /\ ps ) -> ch ) )
Theorem	impexp 259	Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
|- ( ( ( ph /\ ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) )
Theorem	pm3.21 260	Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ps -> ( ps /\ ph ) ) )
Theorem	pm3.22 261	Theorem *3.22 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
|- ( ( ph /\ ps ) -> ( ps /\ ph ) )
Theorem	ancom 262	Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf Lammen, 4-Nov-2012.)
|- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
Theorem	ancomd 263	Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.)
|- ( ph -> ( ps /\ ch ) )   =>    |- ( ph -> ( ch /\ ps ) )
Theorem	ancoms 264	Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ps /\ ph ) -> ch )
Theorem	ancomsd 265	Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)
|- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ph -> ( ( ch /\ ps ) -> th ) )
Theorem	pm3.2i 266	Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.)
|- ph   &    |- ps   =>    |- ( ph /\ ps )
Theorem	pm3.43i 267	Nested conjunction of antecedents. (Contributed by NM, 5-Aug-1993.)
|- ( ( ph -> ps ) -> ( ( ph -> ch ) -> ( ph -> ( ps /\ ch ) ) ) )
Theorem	simplbi 268	Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ph -> ps )
Theorem	simprbi 269	Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ph -> ch )
Theorem	adantr 270	Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.)
|- ( ph -> ps )   =>    |- ( ( ph /\ ch ) -> ps )
Theorem	adantl 271	Inference adding a conjunct to the left of an antecedent. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
|- ( ph -> ps )   =>    |- ( ( ch /\ ph ) -> ps )
Theorem	adantld 272	Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ( th /\ ps ) -> ch ) )
Theorem	adantrd 273	Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ( ps /\ th ) -> ch ) )
Theorem	impel 274	An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.)
|- ( ph -> ( ps -> ch ) )   &    |- ( th -> ps )   =>    |- ( ( ph /\ th ) -> ch )
Theorem	mpan9 275	Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- ( ph -> ps )   &    |- ( ch -> ( ps -> th ) )   =>    |- ( ( ph /\ ch ) -> th )
Theorem	syldan 276	A syllogism deduction with conjoined antecents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ ch ) -> th )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	sylan 277	A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
|- ( ph -> ps )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ( ph /\ ch ) -> th )
Theorem	sylanb 278	A syllogism inference. (Contributed by NM, 18-May-1994.)
|- ( ph <-> ps )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ( ph /\ ch ) -> th )
Theorem	sylanbr 279	A syllogism inference. (Contributed by NM, 18-May-1994.)
|- ( ps <-> ph )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ( ph /\ ch ) -> th )
Theorem	sylan2 280	A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
|- ( ph -> ch )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ( ps /\ ph ) -> th )
Theorem	sylan2b 281	A syllogism inference. (Contributed by NM, 21-Apr-1994.)
|- ( ph <-> ch )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ( ps /\ ph ) -> th )
Theorem	sylan2br 282	A syllogism inference. (Contributed by NM, 21-Apr-1994.)
|- ( ch <-> ph )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ( ps /\ ph ) -> th )
Theorem	syl2an 283	A double syllogism inference. (Contributed by NM, 31-Jan-1997.)
|- ( ph -> ps )   &    |- ( ta -> ch )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ( ph /\ ta ) -> th )
Theorem	syl2anr 284	A double syllogism inference. (Contributed by NM, 17-Sep-2013.)
|- ( ph -> ps )   &    |- ( ta -> ch )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ( ta /\ ph ) -> th )
Theorem	syl2anb 285	A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
|- ( ph <-> ps )   &    |- ( ta <-> ch )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ( ph /\ ta ) -> th )
Theorem	syl2anbr 286	A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
|- ( ps <-> ph )   &    |- ( ch <-> ta )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ( ph /\ ta ) -> th )
Theorem	syland 287	A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ( ch /\ th ) -> ta ) )   =>    |- ( ph -> ( ( ps /\ th ) -> ta ) )
Theorem	sylan2d 288	A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ( th /\ ch ) -> ta ) )   =>    |- ( ph -> ( ( th /\ ps ) -> ta ) )
Theorem	syl2and 289	A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( th -> ta ) )   &    |- ( ph -> ( ( ch /\ ta ) -> et ) )   =>    |- ( ph -> ( ( ps /\ th ) -> et ) )
Theorem	biimpa 290	Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	biimpar 291	Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ( ph /\ ch ) -> ps )
Theorem	biimpac 292	Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ( ps /\ ph ) -> ch )
Theorem	biimparc 293	Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ( ch /\ ph ) -> ps )
Theorem	iba 294	Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.) (Revised by NM, 24-Mar-2013.)
|- ( ph -> ( ps <-> ( ps /\ ph ) ) )
Theorem	ibar 295	Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.) (Revised by NM, 24-Mar-2013.)
|- ( ph -> ( ps <-> ( ph /\ ps ) ) )
Theorem	biantru 296	A wff is equivalent to its conjunction with truth. (Contributed by NM, 5-Aug-1993.)
|- ph   =>    |- ( ps <-> ( ps /\ ph ) )
Theorem	biantrur 297	A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)
|- ph   =>    |- ( ps <-> ( ph /\ ps ) )
Theorem	biantrud 298	A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)
|- ( ph -> ps )   =>    |- ( ph -> ( ch <-> ( ch /\ ps ) ) )
Theorem	biantrurd 299	A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- ( ph -> ps )   =>    |- ( ph -> ( ch <-> ( ps /\ ch ) ) )
Theorem	jca 300	Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   =>    |- ( ph -> ( ps /\ ch ) )