P. 6 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 501-600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ad9antr 501	Deduction adding 9 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ps )
Theorem	ad9antlr 502	Deduction adding 9 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ( ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ps )
Theorem	ad10antr 503	Deduction adding 10 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) /\ ka ) -> ps )
Theorem	ad10antlr 504	Deduction adding 10 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ( ( ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) /\ ka ) -> ps )
Theorem	ad2ant2l 505	Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( th /\ ph ) /\ ( ta /\ ps ) ) -> ch )
Theorem	ad2ant2r 506	Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ph /\ th ) /\ ( ps /\ ta ) ) -> ch )
Theorem	ad2ant2lr 507	Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( th /\ ph ) /\ ( ps /\ ta ) ) -> ch )
Theorem	ad2ant2rl 508	Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ph /\ th ) /\ ( ta /\ ps ) ) -> ch )
Theorem	adantl3r 509	Deduction adding 1 conjunct to antecedent. (Contributed by Alan Sare, 17-Oct-2017.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ( ( ph /\ et ) /\ ps ) /\ ch ) /\ th ) -> ta )
Theorem	ad4ant13 510	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ( ph /\ th ) /\ ps ) /\ ta ) -> ch )
Theorem	ad4ant14 511	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ( ph /\ th ) /\ ta ) /\ ps ) -> ch )
Theorem	ad4ant23 512	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ( th /\ ph ) /\ ps ) /\ ta ) -> ch )
Theorem	ad4ant24 513	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ( th /\ ph ) /\ ta ) /\ ps ) -> ch )
Theorem	adantl4r 514	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( ( ( ( ph /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )   =>    |- ( ( ( ( ( ( ph /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )
Theorem	ad5ant12 515	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ( ( ph /\ ps ) /\ th ) /\ ta ) /\ et ) -> ch )
Theorem	ad5ant13 516	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ( ( ph /\ th ) /\ ps ) /\ ta ) /\ et ) -> ch )
Theorem	ad5ant14 517	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ( ( ph /\ th ) /\ ta ) /\ ps ) /\ et ) -> ch )
Theorem	ad5ant15 518	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ( ( ph /\ th ) /\ ta ) /\ et ) /\ ps ) -> ch )
Theorem	ad5ant23 519	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ( ( th /\ ph ) /\ ps ) /\ ta ) /\ et ) -> ch )
Theorem	ad5ant24 520	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ( ( th /\ ph ) /\ ta ) /\ ps ) /\ et ) -> ch )
Theorem	ad5ant25 521	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ( ( th /\ ph ) /\ ta ) /\ et ) /\ ps ) -> ch )
Theorem	adantl5r 522	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( ( ( ( ( ph /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )   =>    |- ( ( ( ( ( ( ( ph /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )
Theorem	adantl6r 523	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( ( ( ( ( ( ph /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )   =>    |- ( ( ( ( ( ( ( ( ph /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )
Theorem	simpll 524	Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
|- ( ( ( ph /\ ps ) /\ ch ) -> ph )
Theorem	simplr 525	Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)
|- ( ( ( ph /\ ps ) /\ ch ) -> ps )
Theorem	simprl 526	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
|- ( ( ph /\ ( ps /\ ch ) ) -> ps )
Theorem	simprr 527	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
|- ( ( ph /\ ( ps /\ ch ) ) -> ch )
Theorem	simplll 528	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ph )
Theorem	simpllr 529	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )
Theorem	simplrl 530	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )
Theorem	simplrr 531	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ch )
Theorem	simprll 532	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ps )
Theorem	simprlr 533	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ch )
Theorem	simprrl 534	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ch )
Theorem	simprrr 535	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> th )
Theorem	simp-4l 536	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ph )
Theorem	simp-4r 537	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ps )
Theorem	simp-5l 538	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) -> ph )
Theorem	simp-5r 539	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )
Theorem	simp-6l 540	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ph )
Theorem	simp-6r 541	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ps )
Theorem	simp-7l 542	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> ph )
Theorem	simp-7r 543	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> ps )
Theorem	simp-8l 544	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) -> ph )
Theorem	simp-8r 545	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) -> ps )
Theorem	simp-9l 546	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) -> ph )
Theorem	simp-9r 547	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) -> ps )
Theorem	simp-10l 548	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ph )
Theorem	simp-10r 549	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ps )
Theorem	simp-11l 550	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) /\ ka ) -> ph )
Theorem	simp-11r 551	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) /\ ka ) -> ps )
Theorem	pm4.87 552	Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Eric Schmidt, 26-Oct-2006.)
|- ( ( ( ( ( ph /\ ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) /\ ( ( ph -> ( ps -> ch ) ) <-> ( ps -> ( ph -> ch ) ) ) ) /\ ( ( ps -> ( ph -> ch ) ) <-> ( ( ps /\ ph ) -> ch ) ) )
Theorem	a2and 553	Deduction distributing a conjunction as embedded antecedent. (Contributed by AV, 25-Oct-2019.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
|- ( ph -> ( ( ps /\ rh ) -> ( ta -> th ) ) )   &    |- ( ph -> ( ( ps /\ rh ) -> ch ) )   =>    |- ( ph -> ( ( ( ps /\ ch ) -> ta ) -> ( ( ps /\ rh ) -> th ) ) )
Theorem	animpimp2impd 554	Deduction deriving nested implications from conjunctions. (Contributed by AV, 21-Aug-2022.)
|- ( ( ps /\ ph ) -> ( ch -> ( th -> et ) ) )   &    |- ( ( ps /\ ( ph /\ th ) ) -> ( et -> ta ) )   =>    |- ( ph -> ( ( ps -> ch ) -> ( ps -> ( th -> ta ) ) ) )
Theorem	abai 555	Introduce one conjunct as an antecedent to the other. "abai" stands for "and, biconditional, and, implication". (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)
|- ( ( ph /\ ps ) <-> ( ph /\ ( ph -> ps ) ) )
Theorem	an12 556	Swap two conjuncts. Note that the first digit (1) in the label refers to the outer conjunct position, and the next digit (2) to the inner conjunct position. (Contributed by NM, 12-Mar-1995.)
|- ( ( ph /\ ( ps /\ ch ) ) <-> ( ps /\ ( ph /\ ch ) ) )
Theorem	an32 557	A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
|- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ph /\ ch ) /\ ps ) )
Theorem	an13 558	A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
|- ( ( ph /\ ( ps /\ ch ) ) <-> ( ch /\ ( ps /\ ph ) ) )
Theorem	an31 559	A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
|- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ch /\ ps ) /\ ph ) )
Theorem	an12s 560	Swap two conjuncts in antecedent. The label suffix "s" means that an12 556 is combined with syl 14 (or a variant). (Contributed by NM, 13-Mar-1996.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ps /\ ( ph /\ ch ) ) -> th )
Theorem	ancom2s 561	Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ( ch /\ ps ) ) -> th )
Theorem	an13s 562	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ch /\ ( ps /\ ph ) ) -> th )
Theorem	an32s 563	Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ph /\ ch ) /\ ps ) -> th )
Theorem	ancom1s 564	Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ps /\ ph ) /\ ch ) -> th )
Theorem	an31s 565	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ch /\ ps ) /\ ph ) -> th )
Theorem	anass1rs 566	Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ( ph /\ ch ) /\ ps ) -> th )
Theorem	anabs1 567	Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
|- ( ( ( ph /\ ps ) /\ ph ) <-> ( ph /\ ps ) )
Theorem	anabs5 568	Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
|- ( ( ph /\ ( ph /\ ps ) ) <-> ( ph /\ ps ) )
Theorem	anabs7 569	Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 17-Nov-2013.)
|- ( ( ps /\ ( ph /\ ps ) ) <-> ( ph /\ ps ) )
Theorem	anabsan 570	Absorption of antecedent with conjunction. (Contributed by NM, 24-Mar-1996.) (Revised by NM, 18-Nov-2013.)
|- ( ( ( ph /\ ph ) /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabss1 571	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
|- ( ( ( ph /\ ps ) /\ ph ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabss4 572	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.)
|- ( ( ( ps /\ ph ) /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabss5 573	Absorption of antecedent into conjunction. (Contributed by NM, 10-May-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
|- ( ( ph /\ ( ph /\ ps ) ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabsi5 574	Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
|- ( ph -> ( ( ph /\ ps ) -> ch ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabsi6 575	Absorption of antecedent into conjunction. (Contributed by NM, 14-Aug-2000.)
|- ( ph -> ( ( ps /\ ph ) -> ch ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabsi7 576	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
|- ( ps -> ( ( ph /\ ps ) -> ch ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabsi8 577	Absorption of antecedent into conjunction. (Contributed by NM, 26-Sep-1999.)
|- ( ps -> ( ( ps /\ ph ) -> ch ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabss7 578	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 19-Nov-2013.)
|- ( ( ps /\ ( ph /\ ps ) ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabsan2 579	Absorption of antecedent with conjunction. (Contributed by NM, 10-May-2004.) (Revised by NM, 1-Jan-2013.)
|- ( ( ph /\ ( ps /\ ps ) ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabss3 580	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
|- ( ( ( ph /\ ps ) /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	an4 581	Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch ) /\ ( ps /\ th ) ) )
Theorem	an42 582	Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch ) /\ ( th /\ ps ) ) )
Theorem	an4s 583	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
Theorem	an42s 584	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ( ph /\ ch ) /\ ( th /\ ps ) ) -> ta )
Theorem	anandi 585	Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
|- ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
Theorem	anandir 586	Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ph /\ ch ) /\ ( ps /\ ch ) ) )
Theorem	anandis 587	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
|- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) -> ta )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> ta )
Theorem	anandirs 588	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
|- ( ( ( ph /\ ch ) /\ ( ps /\ ch ) ) -> ta )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> ta )
Theorem	syl2an2 589	syl2an 287 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
|- ( ph -> ps )   &    |- ( ( ch /\ ph ) -> th )   &    |- ( ( ps /\ th ) -> ta )   =>    |- ( ( ch /\ ph ) -> ta )
Theorem	syl2an2r 590	syl2anr 288 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
|- ( ph -> ps )   &    |- ( ( ph /\ ch ) -> th )   &    |- ( ( ps /\ th ) -> ta )   =>    |- ( ( ph /\ ch ) -> ta )
Theorem	impbida 591	Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ ch ) -> ps )   =>    |- ( ph -> ( ps <-> ch ) )
Theorem	pm3.45 592	Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ps ) -> ( ( ph /\ ch ) -> ( ps /\ ch ) ) )
Theorem	im2anan9 593	Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
|- ( ph -> ( ps -> ch ) )   &    |- ( th -> ( ta -> et ) )   =>    |- ( ( ph /\ th ) -> ( ( ps /\ ta ) -> ( ch /\ et ) ) )
Theorem	im2anan9r 594	Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
|- ( ph -> ( ps -> ch ) )   &    |- ( th -> ( ta -> et ) )   =>    |- ( ( th /\ ph ) -> ( ( ps /\ ta ) -> ( ch /\ et ) ) )
Theorem	anim12dan 595	Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ th ) -> ta )   =>    |- ( ( ph /\ ( ps /\ th ) ) -> ( ch /\ ta ) )
Theorem	pm5.1 596	Two propositions are equivalent if they are both true. Theorem *5.1 of [WhiteheadRussell] p. 123. (Contributed by NM, 21-May-1994.)
|- ( ( ph /\ ps ) -> ( ph <-> ps ) )
Theorem	pm3.43 597	Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 27-Nov-2013.)
|- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) -> ( ph -> ( ps /\ ch ) ) )
Theorem	jcab 598	Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 27-Nov-2013.)
|- ( ( ph -> ( ps /\ ch ) ) <-> ( ( ph -> ps ) /\ ( ph -> ch ) ) )
Theorem	pm4.76 599	Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) <-> ( ph -> ( ps /\ ch ) ) )
Theorem	pm4.38 600	Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph <-> ch ) /\ ( ps <-> th ) ) -> ( ( ph /\ ps ) <-> ( ch /\ th ) ) )