P. 4 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 301-400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ibar 301	Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.) (Revised by NM, 24-Mar-2013.)
|- ( ph -> ( ps <-> ( ph /\ ps ) ) )
Theorem	biantru 302	A wff is equivalent to its conjunction with truth. (Contributed by NM, 5-Aug-1993.)
|- ph   =>    |- ( ps <-> ( ps /\ ph ) )
Theorem	biantrur 303	A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)
|- ph   =>    |- ( ps <-> ( ph /\ ps ) )
Theorem	biantrud 304	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 305	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 306	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 ) )
Theorem	jcad 307	Deduction conjoining the consequents of two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ps -> th ) )   =>    |- ( ph -> ( ps -> ( ch /\ th ) ) )
Theorem	jca2 308	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ps -> th )   =>    |- ( ph -> ( ps -> ( ch /\ th ) ) )
Theorem	jca31 309	Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   =>    |- ( ph -> ( ( ps /\ ch ) /\ th ) )
Theorem	jca32 310	Join three consequents. (Contributed by FL, 1-Aug-2009.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   =>    |- ( ph -> ( ps /\ ( ch /\ th ) ) )
Theorem	jcai 311	Deduction replacing implication with conjunction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps /\ ch ) )
Theorem	jctil 312	Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
|- ( ph -> ps )   &    |- ch   =>    |- ( ph -> ( ch /\ ps ) )
Theorem	jctir 313	Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
|- ( ph -> ps )   &    |- ch   =>    |- ( ph -> ( ps /\ ch ) )
Theorem	jctl 314	Inference conjoining a theorem to the left of a consequent. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.)
|- ps   =>    |- ( ph -> ( ps /\ ph ) )
Theorem	jctr 315	Inference conjoining a theorem to the right of a consequent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.)
|- ps   =>    |- ( ph -> ( ph /\ ps ) )
Theorem	jctild 316	Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> th )   =>    |- ( ph -> ( ps -> ( th /\ ch ) ) )
Theorem	jctird 317	Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> th )   =>    |- ( ph -> ( ps -> ( ch /\ th ) ) )
Theorem	ancl 318	Conjoin antecedent to left of consequent. (Contributed by NM, 15-Aug-1994.)
|- ( ( ph -> ps ) -> ( ph -> ( ph /\ ps ) ) )
Theorem	anclb 319	Conjoin antecedent to left of consequent. Theorem *4.7 of [WhiteheadRussell] p. 120. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
|- ( ( ph -> ps ) <-> ( ph -> ( ph /\ ps ) ) )
Theorem	pm5.42 320	Theorem *5.42 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ( ps -> ch ) ) <-> ( ph -> ( ps -> ( ph /\ ch ) ) ) )
Theorem	ancr 321	Conjoin antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
|- ( ( ph -> ps ) -> ( ph -> ( ps /\ ph ) ) )
Theorem	ancrb 322	Conjoin antecedent to right of consequent. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
|- ( ( ph -> ps ) <-> ( ph -> ( ps /\ ph ) ) )
Theorem	ancli 323	Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.)
|- ( ph -> ps )   =>    |- ( ph -> ( ph /\ ps ) )
Theorem	ancri 324	Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
|- ( ph -> ps )   =>    |- ( ph -> ( ps /\ ph ) )
Theorem	ancld 325	Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> ( ps /\ ch ) ) )
Theorem	ancrd 326	Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> ( ch /\ ps ) ) )
Theorem	anc2l 327	Conjoin antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 14-Jul-2013.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ( ph /\ ch ) ) ) )
Theorem	anc2r 328	Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ( ch /\ ph ) ) ) )
Theorem	anc2li 329	Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> ( ph /\ ch ) ) )
Theorem	anc2ri 330	Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> ( ch /\ ph ) ) )
Theorem	pm3.41 331	Theorem *3.41 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ch ) -> ( ( ph /\ ps ) -> ch ) )
Theorem	pm3.42 332	Theorem *3.42 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- ( ( ps -> ch ) -> ( ( ph /\ ps ) -> ch ) )
Theorem	pm3.4 333	Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113. (Contributed by NM, 31-Jul-1995.)
|- ( ( ph /\ ps ) -> ( ph -> ps ) )
Theorem	pm4.45im 334	Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.)
|- ( ph <-> ( ph /\ ( ps -> ph ) ) )
Theorem	anim12d 335	Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( th -> ta ) )   =>    |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )
Theorem	anim1d 336	Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ( ps /\ th ) -> ( ch /\ th ) ) )
Theorem	anim2d 337	Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ( th /\ ps ) -> ( th /\ ch ) ) )
Theorem	anim12i 338	Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)
|- ( ph -> ps )   &    |- ( ch -> th )   =>    |- ( ( ph /\ ch ) -> ( ps /\ th ) )
Theorem	anim12ci 339	Variant of anim12i 338 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> ps )   &    |- ( ch -> th )   =>    |- ( ( ph /\ ch ) -> ( th /\ ps ) )
Theorem	anim1i 340	Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   =>    |- ( ( ph /\ ch ) -> ( ps /\ ch ) )
Theorem	anim1ci 341	Introduce conjunct to both sides of an implication. (Contributed by Peter Mazsa, 24-Sep-2022.)
|- ( ph -> ps )   =>    |- ( ( ph /\ ch ) -> ( ch /\ ps ) )
Theorem	anim2i 342	Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   =>    |- ( ( ch /\ ph ) -> ( ch /\ ps ) )
Theorem	anim12ii 343	Conjoin antecedents and consequents in a deduction. (Contributed by NM, 11-Nov-2007.) (Proof shortened by Wolf Lammen, 19-Jul-2013.)
|- ( ph -> ( ps -> ch ) )   &    |- ( th -> ( ps -> ta ) )   =>    |- ( ( ph /\ th ) -> ( ps -> ( ch /\ ta ) ) )
Theorem	anim12 344	Theorem *3.47 of [WhiteheadRussell] p. 113. It was proved by Leibniz, and it evidently pleased him enough to call it 'praeclarum theorema' (splendid theorem). (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
|- ( ( ( ph -> ps ) /\ ( ch -> th ) ) -> ( ( ph /\ ch ) -> ( ps /\ th ) ) )
Theorem	pm3.33 345	Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ps -> ch ) ) -> ( ph -> ch ) )
Theorem	pm3.34 346	Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ps -> ch ) /\ ( ph -> ps ) ) -> ( ph -> ch ) )
Theorem	pm3.35 347	Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. (Contributed by NM, 14-Dec-2002.)
|- ( ( ph /\ ( ph -> ps ) ) -> ps )
Theorem	pm5.31 348	Theorem *5.31 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ch /\ ( ph -> ps ) ) -> ( ph -> ( ps /\ ch ) ) )
Theorem	imp4a 349	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ph -> ( ps -> ( ( ch /\ th ) -> ta ) ) )
Theorem	imp4b 350	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ph /\ ps ) -> ( ( ch /\ th ) -> ta ) )
Theorem	imp4c 351	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ph -> ( ( ( ps /\ ch ) /\ th ) -> ta ) )
Theorem	imp4d 352	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ph -> ( ( ps /\ ( ch /\ th ) ) -> ta ) )
Theorem	imp41 353	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )
Theorem	imp42 354	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ta )
Theorem	imp43 355	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
Theorem	imp44 356	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ta )
Theorem	imp45 357	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ta )
Theorem	imp5a 358	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ph -> ( ps -> ( ch -> ( ( th /\ ta ) -> et ) ) ) )
Theorem	imp5d 359	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> ( ( th /\ ta ) -> et ) )
Theorem	imp5g 360	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ( ph /\ ps ) -> ( ( ( ch /\ th ) /\ ta ) -> et ) )
Theorem	imp55 361	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) /\ ta ) -> et )
Theorem	imp511 362	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ( ph /\ ( ( ps /\ ( ch /\ th ) ) /\ ta ) ) -> et )
Theorem	expimpd 363	Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)
|- ( ( ph /\ ps ) -> ( ch -> th ) )   =>    |- ( ph -> ( ( ps /\ ch ) -> th ) )
Theorem	exp31 364	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ph -> ( ps -> ( ch -> th ) ) )
Theorem	exp32 365	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ph -> ( ps -> ( ch -> th ) ) )
Theorem	exp4a 366	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ( ch /\ th ) -> ta ) ) )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp4b 367	An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
|- ( ( ph /\ ps ) -> ( ( ch /\ th ) -> ta ) )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp4c 368	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ( ( ps /\ ch ) /\ th ) -> ta ) )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp4d 369	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ( ps /\ ( ch /\ th ) ) -> ta ) )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp41 370	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp42 371	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp43 372	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp44 373	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp45 374	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	expr 375	Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ps ) -> ( ch -> th ) )
Theorem	exp5c 376	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ph -> ( ( ps /\ ch ) -> ( ( th /\ ta ) -> et ) ) )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )
Theorem	exp53 377	An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ( ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) /\ ta ) -> et )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )
Theorem	expl 378	Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ph -> ( ( ps /\ ch ) -> th ) )
Theorem	impr 379	Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ( ( ph /\ ps ) -> ( ch -> th ) )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> th )
Theorem	impl 380	Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> th )
Theorem	impac 381	Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ( ph /\ ps ) -> ( ch /\ ps ) )
Theorem	exbiri 382	Inference form of exbir 1447. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.)
|- ( ( ph /\ ps ) -> ( ch <-> th ) )   =>    |- ( ph -> ( ps -> ( th -> ch ) ) )
Theorem	simprbda 383	Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	simplbda 384	Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	simplbi2 385	Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ch -> ph ) )
Theorem	simpl2im 386	Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021.)
|- ( ph -> ( ps /\ ch ) )   &    |- ( ch -> th )   =>    |- ( ph -> th )
Theorem	simplbiim 387	Implication from an eliminated conjunct equivalent to the antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch ) )   &    |- ( ch -> th )   =>    |- ( ph -> th )
Theorem	dfbi2 388	A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.)
|- ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) )
Theorem	pm4.71 389	Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)
|- ( ( ph -> ps ) <-> ( ph <-> ( ph /\ ps ) ) )
Theorem	pm4.71r 390	Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 25-Jul-1999.)
|- ( ( ph -> ps ) <-> ( ph <-> ( ps /\ ph ) ) )
Theorem	pm4.71i 391	Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.)
|- ( ph -> ps )   =>    |- ( ph <-> ( ph /\ ps ) )
Theorem	pm4.71ri 392	Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.)
|- ( ph -> ps )   =>    |- ( ph <-> ( ps /\ ph ) )
Theorem	pm4.71d 393	Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps <-> ( ps /\ ch ) ) )
Theorem	pm4.71rd 394	Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps <-> ( ch /\ ps ) ) )
Theorem	pm4.24 395	Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 14-Mar-2014.)
|- ( ph <-> ( ph /\ ph ) )
Theorem	anidm 396	Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)
|- ( ( ph /\ ph ) <-> ph )
Theorem	anidms 397	Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)
|- ( ( ph /\ ph ) -> ps )   =>    |- ( ph -> ps )
Theorem	anidmdbi 398	Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.)
|- ( ( ph -> ( ps /\ ps ) ) <-> ( ph -> ps ) )
Theorem	anasss 399	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> th )
Theorem	anassrs 400	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> th )