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	biantrur 301	A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)
|- ph   =>    |- ( ps <-> ( ph /\ ps ) )
Theorem	biantrud 302	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 303	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 304	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 305	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 306	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 307	Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   =>    |- ( ph -> ( ( ps /\ ch ) /\ th ) )
Theorem	jca32 308	Join three consequents. (Contributed by FL, 1-Aug-2009.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   =>    |- ( ph -> ( ps /\ ( ch /\ th ) ) )
Theorem	jcai 309	Deduction replacing implication with conjunction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps /\ ch ) )
Theorem	jctil 310	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 311	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 312	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 313	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 314	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 315	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 316	Conjoin antecedent to left of consequent. (Contributed by NM, 15-Aug-1994.)
|- ( ( ph -> ps ) -> ( ph -> ( ph /\ ps ) ) )
Theorem	anclb 317	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 318	Theorem *5.42 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ( ps -> ch ) ) <-> ( ph -> ( ps -> ( ph /\ ch ) ) ) )
Theorem	ancr 319	Conjoin antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
|- ( ( ph -> ps ) -> ( ph -> ( ps /\ ph ) ) )
Theorem	ancrb 320	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 321	Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.)
|- ( ph -> ps )   =>    |- ( ph -> ( ph /\ ps ) )
Theorem	ancri 322	Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
|- ( ph -> ps )   =>    |- ( ph -> ( ps /\ ph ) )
Theorem	ancld 323	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 324	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 325	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 326	Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ( ch /\ ph ) ) ) )
Theorem	anc2li 327	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 328	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 329	Theorem *3.41 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ch ) -> ( ( ph /\ ps ) -> ch ) )
Theorem	pm3.42 330	Theorem *3.42 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- ( ( ps -> ch ) -> ( ( ph /\ ps ) -> ch ) )
Theorem	pm3.4 331	Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113. (Contributed by NM, 31-Jul-1995.)
|- ( ( ph /\ ps ) -> ( ph -> ps ) )
Theorem	pm4.45im 332	Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.)
|- ( ph <-> ( ph /\ ( ps -> ph ) ) )
Theorem	anim12d 333	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 334	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 335	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 336	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 337	Variant of anim12i 336 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> ps )   &    |- ( ch -> th )   =>    |- ( ( ph /\ ch ) -> ( th /\ ps ) )
Theorem	anim1i 338	Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   =>    |- ( ( ph /\ ch ) -> ( ps /\ ch ) )
Theorem	anim1ci 339	Introduce conjunct to both sides of an implication. (Contributed by Peter Mazsa, 24-Sep-2022.)
|- ( ph -> ps )   =>    |- ( ( ph /\ ch ) -> ( ch /\ ps ) )
Theorem	anim2i 340	Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   =>    |- ( ( ch /\ ph ) -> ( ch /\ ps ) )
Theorem	anim12ii 341	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 342	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 343	Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ps -> ch ) ) -> ( ph -> ch ) )
Theorem	pm3.34 344	Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ps -> ch ) /\ ( ph -> ps ) ) -> ( ph -> ch ) )
Theorem	pm3.35 345	Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. (Contributed by NM, 14-Dec-2002.)
|- ( ( ph /\ ( ph -> ps ) ) -> ps )
Theorem	pm5.31 346	Theorem *5.31 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ch /\ ( ph -> ps ) ) -> ( ph -> ( ps /\ ch ) ) )
Theorem	imp4a 347	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ph -> ( ps -> ( ( ch /\ th ) -> ta ) ) )
Theorem	imp4b 348	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ph /\ ps ) -> ( ( ch /\ th ) -> ta ) )
Theorem	imp4c 349	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ph -> ( ( ( ps /\ ch ) /\ th ) -> ta ) )
Theorem	imp4d 350	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ph -> ( ( ps /\ ( ch /\ th ) ) -> ta ) )
Theorem	imp41 351	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )
Theorem	imp42 352	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ta )
Theorem	imp43 353	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
Theorem	imp44 354	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ta )
Theorem	imp45 355	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ta )
Theorem	imp5a 356	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ph -> ( ps -> ( ch -> ( ( th /\ ta ) -> et ) ) ) )
Theorem	imp5d 357	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> ( ( th /\ ta ) -> et ) )
Theorem	imp5g 358	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ( ph /\ ps ) -> ( ( ( ch /\ th ) /\ ta ) -> et ) )
Theorem	imp55 359	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) /\ ta ) -> et )
Theorem	imp511 360	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ( ph /\ ( ( ps /\ ( ch /\ th ) ) /\ ta ) ) -> et )
Theorem	expimpd 361	Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)
|- ( ( ph /\ ps ) -> ( ch -> th ) )   =>    |- ( ph -> ( ( ps /\ ch ) -> th ) )
Theorem	exp31 362	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ph -> ( ps -> ( ch -> th ) ) )
Theorem	exp32 363	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ph -> ( ps -> ( ch -> th ) ) )
Theorem	exp4a 364	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ps -> ( ( ch /\ th ) -> ta ) ) )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp4b 365	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 366	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ( ( ps /\ ch ) /\ th ) -> ta ) )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp4d 367	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ph -> ( ( ps /\ ( ch /\ th ) ) -> ta ) )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp41 368	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp42 369	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp43 370	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp44 371	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp45 372	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	expr 373	Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ps ) -> ( ch -> th ) )
Theorem	exp5c 374	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ph -> ( ( ps /\ ch ) -> ( ( th /\ ta ) -> et ) ) )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )
Theorem	exp53 375	An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ( ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) /\ ta ) -> et )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )
Theorem	expl 376	Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ph -> ( ( ps /\ ch ) -> th ) )
Theorem	impr 377	Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ( ( ph /\ ps ) -> ( ch -> th ) )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> th )
Theorem	impl 378	Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> th )
Theorem	impac 379	Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ( ph /\ ps ) -> ( ch /\ ps ) )
Theorem	exbiri 380	Inference form of exbir 1429. (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 381	Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	simplbda 382	Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	simplbi2 383	Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ch -> ph ) )
Theorem	simpl2im 384	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 385	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 386	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 387	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 388	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 389	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 390	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 391	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 392	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 393	Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 14-Mar-2014.)
|- ( ph <-> ( ph /\ ph ) )
Theorem	anidm 394	Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)
|- ( ( ph /\ ph ) <-> ph )
Theorem	anidms 395	Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)
|- ( ( ph /\ ph ) -> ps )   =>    |- ( ph -> ps )
Theorem	anidmdbi 396	Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.)
|- ( ( ph -> ( ps /\ ps ) ) <-> ( ph -> ps ) )
Theorem	anasss 397	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 398	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> th )
Theorem	anass 399	Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
Theorem	sylanl1 400	A syllogism inference. (Contributed by NM, 10-Mar-2005.)
|- ( ph -> ps )   &    |- ( ( ( ps /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ph /\ ch ) /\ th ) -> ta )