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	ad2ant2r 501	Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ph /\ th ) /\ ( ps /\ ta ) ) -> ch )
Theorem	ad2ant2lr 502	Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( th /\ ph ) /\ ( ps /\ ta ) ) -> ch )
Theorem	ad2ant2rl 503	Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ph /\ th ) /\ ( ta /\ ps ) ) -> ch )
Theorem	adantl3r 504	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 505	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 506	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 507	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 508	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 509	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 510	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ( ( ph /\ ps ) /\ th ) /\ ta ) /\ et ) -> ch )
Theorem	ad5ant13 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 ) /\ ps ) /\ ta ) /\ et ) -> ch )
Theorem	ad5ant14 512	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 513	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 514	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 515	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 516	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 517	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 518	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 519	Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
|- ( ( ( ph /\ ps ) /\ ch ) -> ph )
Theorem	simplr 520	Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)
|- ( ( ( ph /\ ps ) /\ ch ) -> ps )
Theorem	simprl 521	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
|- ( ( ph /\ ( ps /\ ch ) ) -> ps )
Theorem	simprr 522	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
|- ( ( ph /\ ( ps /\ ch ) ) -> ch )
Theorem	simplll 523	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ph )
Theorem	simpllr 524	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )
Theorem	simplrl 525	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )
Theorem	simplrr 526	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ch )
Theorem	simprll 527	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ps )
Theorem	simprlr 528	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ch )
Theorem	simprrl 529	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ch )
Theorem	simprrr 530	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> th )
Theorem	simp-4l 531	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ph )
Theorem	simp-4r 532	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ps )
Theorem	simp-5l 533	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) -> ph )
Theorem	simp-5r 534	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )
Theorem	simp-6l 535	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ph )
Theorem	simp-6r 536	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ps )
Theorem	simp-7l 537	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> ph )
Theorem	simp-7r 538	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> ps )
Theorem	simp-8l 539	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) -> ph )
Theorem	simp-8r 540	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) -> ps )
Theorem	simp-9l 541	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 542	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 543	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 544	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 545	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 546	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 547	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 548	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 549	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 550	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 551	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 552	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 553	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 554	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 555	Swap two conjuncts in antecedent. The label suffix "s" means that an12 551 is combined with syl 14 (or a variant). (Contributed by NM, 13-Mar-1996.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ps /\ ( ph /\ ch ) ) -> th )
Theorem	ancom2s 556	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 557	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ch /\ ( ps /\ ph ) ) -> th )
Theorem	an32s 558	Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ph /\ ch ) /\ ps ) -> th )
Theorem	ancom1s 559	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 560	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ch /\ ps ) /\ ph ) -> th )
Theorem	anass1rs 561	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 562	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 563	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 564	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 565	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 566	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 567	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.)
|- ( ( ( ps /\ ph ) /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabss5 568	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 569	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 570	Absorption of antecedent into conjunction. (Contributed by NM, 14-Aug-2000.)
|- ( ph -> ( ( ps /\ ph ) -> ch ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabsi7 571	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 572	Absorption of antecedent into conjunction. (Contributed by NM, 26-Sep-1999.)
|- ( ps -> ( ( ps /\ ph ) -> ch ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabss7 573	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 574	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 575	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 576	Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch ) /\ ( ps /\ th ) ) )
Theorem	an42 577	Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch ) /\ ( th /\ ps ) ) )
Theorem	an4s 578	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
Theorem	an42s 579	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ( ph /\ ch ) /\ ( th /\ ps ) ) -> ta )
Theorem	anandi 580	Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
|- ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
Theorem	anandir 581	Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ph /\ ch ) /\ ( ps /\ ch ) ) )
Theorem	anandis 582	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
|- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) -> ta )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> ta )
Theorem	anandirs 583	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
|- ( ( ( ph /\ ch ) /\ ( ps /\ ch ) ) -> ta )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> ta )
Theorem	syl2an2 584	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 585	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 586	Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ ch ) -> ps )   =>    |- ( ph -> ( ps <-> ch ) )
Theorem	pm3.45 587	Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ps ) -> ( ( ph /\ ch ) -> ( ps /\ ch ) ) )
Theorem	im2anan9 588	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 589	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 590	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 591	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 592	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 593	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 594	Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) <-> ( ph -> ( ps /\ ch ) ) )
Theorem	pm4.38 595	Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph <-> ch ) /\ ( ps <-> th ) ) -> ( ( ph /\ ps ) <-> ( ch /\ th ) ) )
Theorem	bi2anan9 596	Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( th -> ( ta <-> et ) )   =>    |- ( ( ph /\ th ) -> ( ( ps /\ ta ) <-> ( ch /\ et ) ) )
Theorem	bi2anan9r 597	Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( th -> ( ta <-> et ) )   =>    |- ( ( th /\ ph ) -> ( ( ps /\ ta ) <-> ( ch /\ et ) ) )
Theorem	bi2bian9 598	Deduction joining two biconditionals with different antecedents. (Contributed by NM, 12-May-2004.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( th -> ( ta <-> et ) )   =>    |- ( ( ph /\ th ) -> ( ( ps <-> ta ) <-> ( ch <-> et ) ) )
Theorem	pm5.33 599	Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph /\ ( ps -> ch ) ) <-> ( ph /\ ( ( ph /\ ps ) -> ch ) ) )
Theorem	pm5.36 600	Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph /\ ( ph <-> ps ) ) <-> ( ps /\ ( ph <-> ps ) ) )