P. 7 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 601-700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	expl 601	Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)
|- (((ph /\ ps) /\ ch) -> th)   =>   |- (ph -> ((ps /\ ch) -> th))
Theorem	impr 602	Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ((ph /\ ps) -> (ch -> th))   =>   |- ((ph /\ (ps /\ ch)) -> th)
Theorem	impl 603	Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- (ph -> ((ps /\ ch) -> th))   =>   |- (((ph /\ ps) /\ ch) -> th)
Theorem	impac 604	Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994.)
|- (ph -> (ps -> ch))   =>   |- ((ph /\ ps) -> (ch /\ ps))
Theorem	exbiri 605	Inference form of exbir 1365. This proof is exbiriVD in set.mm automatically translated and minimized. (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 606	Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
|- (ph -> (ps <-> (ch /\ th)))   =>   |- ((ph /\ ps) -> ch)
Theorem	simplbda 607	Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
|- (ph -> (ps <-> (ch /\ th)))   =>   |- ((ph /\ ps) -> th)
Theorem	simplbi2 608	Deduction eliminating a conjunct. Automatically derived from simplbi2VD in set.mm. (Contributed by Alan Sare, 31-Dec-2011.)
|- (ph <-> (ps /\ ch))   =>   |- (ps -> (ch -> ph))
Theorem	dfbi2 609	A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 5-Aug-1993.)
|- ((ph <-> ps) <-> ((ph -> ps) /\ (ps -> ph)))
Theorem	dfbi 610	Definition df-bi 177 rewritten in an abbreviated form to help intuitive understanding of that definition. Note that it is a conjunction of two implications; one which asserts properties that follow from the biconditional and one which asserts properties that imply the biconditional. (Contributed by NM, 15-Aug-2008.)
|- (((ph <-> ps) -> ((ph -> ps) /\ (ps -> ph))) /\ (((ph -> ps) /\ (ps -> ph)) -> (ph <-> ps)))
Theorem	pm4.71 611	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 612	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 613	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 614	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 615	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 616	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	pm5.32 617	Distribution of implication over biconditional. Theorem *5.32 of [WhiteheadRussell] p. 125. (Contributed by NM, 1-Aug-1994.)
|- ((ph -> (ps <-> ch)) <-> ((ph /\ ps) <-> (ph /\ ch)))
Theorem	pm5.32i 618	Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.)
|- (ph -> (ps <-> ch))   =>   |- ((ph /\ ps) <-> (ph /\ ch))
Theorem	pm5.32ri 619	Distribution of implication over biconditional (inference rule). (Contributed by NM, 12-Mar-1995.)
|- (ph -> (ps <-> ch))   =>   |- ((ps /\ ph) <-> (ch /\ ph))
Theorem	pm5.32d 620	Distribution of implication over biconditional (deduction rule). (Contributed by NM, 29-Oct-1996.)
|- (ph -> (ps -> (ch <-> th)))   =>   |- (ph -> ((ps /\ ch) <-> (ps /\ th)))
Theorem	pm5.32rd 621	Distribution of implication over biconditional (deduction rule). (Contributed by NM, 25-Dec-2004.)
|- (ph -> (ps -> (ch <-> th)))   =>   |- (ph -> ((ch /\ ps) <-> (th /\ ps)))
Theorem	pm5.32da 622	Distribution of implication over biconditional (deduction rule). (Contributed by NM, 9-Dec-2006.)
|- ((ph /\ ps) -> (ch <-> th))   =>   |- (ph -> ((ps /\ ch) <-> (ps /\ th)))
Theorem	biadan2 623	Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.)
|- (ph -> ps)   &   |- (ps -> (ph <-> ch))   =>   |- (ph <-> (ps /\ ch))
Theorem	pm4.24 624	Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
|- (ph <-> (ph /\ ph))
Theorem	anidm 625	Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)
|- ((ph /\ ph) <-> ph)
Theorem	anidms 626	Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)
|- ((ph /\ ph) -> ps)   =>   |- (ph -> ps)
Theorem	anidmdbi 627	Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.)
|- ((ph -> (ps /\ ps)) <-> (ph -> ps))
Theorem	anasss 628	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 629	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 630	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 631	A syllogism inference. (Contributed by NM, 10-Mar-2005.)
|- (ph -> ps)   &   |- (((ps /\ ch) /\ th) -> ta)   =>   |- (((ph /\ ch) /\ th) -> ta)
Theorem	sylanl2 632	A syllogism inference. (Contributed by NM, 1-Jan-2005.)
|- (ph -> ch)   &   |- (((ps /\ ch) /\ th) -> ta)   =>   |- (((ps /\ ph) /\ th) -> ta)
Theorem	sylanr1 633	A syllogism inference. (Contributed by NM, 9-Apr-2005.)
|- (ph -> ch)   &   |- ((ps /\ (ch /\ th)) -> ta)   =>   |- ((ps /\ (ph /\ th)) -> ta)
Theorem	sylanr2 634	A syllogism inference. (Contributed by NM, 9-Apr-2005.)
|- (ph -> th)   &   |- ((ps /\ (ch /\ th)) -> ta)   =>   |- ((ps /\ (ch /\ ph)) -> ta)
Theorem	sylani 635	A syllogism inference. (Contributed by NM, 2-May-1996.)
|- (ph -> ch)   &   |- (ps -> ((ch /\ th) -> ta))   =>   |- (ps -> ((ph /\ th) -> ta))
Theorem	sylan2i 636	A syllogism inference. (Contributed by NM, 1-Aug-1994.)
|- (ph -> th)   &   |- (ps -> ((ch /\ th) -> ta))   =>   |- (ps -> ((ch /\ ph) -> ta))
Theorem	syl2ani 637	A syllogism inference. (Contributed by NM, 3-Aug-1999.)
|- (ph -> ch)   &   |- (et -> th)   &   |- (ps -> ((ch /\ th) -> ta))   =>   |- (ps -> ((ph /\ et) -> ta))
Theorem	sylan9 638	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- (ph -> (ps -> ch))   &   |- (th -> (ch -> ta))   =>   |- ((ph /\ th) -> (ps -> ta))
Theorem	sylan9r 639	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps -> ch))   &   |- (th -> (ch -> ta))   =>   |- ((th /\ ph) -> (ps -> ta))
Theorem	mtand 640	A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
|- (ph -> -. ch)   &   |- ((ph /\ ps) -> ch)   =>   |- (ph -> -. ps)
Theorem	mtord 641	A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.)
|- (ph -> -. ch)   &   |- (ph -> -. th)   &   |- (ph -> (ps -> (ch \/ th)))   =>   |- (ph -> -. ps)
Theorem	syl2anc 642	Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)
|- (ph -> ps)   &   |- (ph -> ch)   &   |- ((ps /\ ch) -> th)   =>   |- (ph -> th)
Theorem	sylancl 643	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- (ph -> ps)   &   |- ch   &   |- ((ps /\ ch) -> th)   =>   |- (ph -> th)
Theorem	sylancr 644	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ps   &   |- (ph -> ch)   &   |- ((ps /\ ch) -> th)   =>   |- (ph -> th)
Theorem	sylanbrc 645	Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- (ph -> ps)   &   |- (ph -> ch)   &   |- (th <-> (ps /\ ch))   =>   |- (ph -> th)
Theorem	sylancb 646	A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)
|- (ph <-> ps)   &   |- (ph <-> ch)   &   |- ((ps /\ ch) -> th)   =>   |- (ph -> th)
Theorem	sylancbr 647	A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)
|- (ps <-> ph)   &   |- (ch <-> ph)   &   |- ((ps /\ ch) -> th)   =>   |- (ph -> th)
Theorem	sylancom 648	Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008.)
|- ((ph /\ ps) -> ch)   &   |- ((ch /\ ps) -> th)   =>   |- ((ph /\ ps) -> th)
Theorem	mpdan 649	An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
|- (ph -> ps)   &   |- ((ph /\ ps) -> ch)   =>   |- (ph -> ch)
Theorem	mpancom 650	An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
|- (ps -> ph)   &   |- ((ph /\ ps) -> ch)   =>   |- (ps -> ch)
Theorem	mpan 651	An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
|- ph   &   |- ((ph /\ ps) -> ch)   =>   |- (ps -> ch)
Theorem	mpan2 652	An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
|- ps   &   |- ((ph /\ ps) -> ch)   =>   |- (ph -> ch)
Theorem	mp2an 653	An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)
|- ph   &   |- ps   &   |- ((ph /\ ps) -> ch)   =>   |- ch
Theorem	mp4an 654	An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.)
|- ph   &   |- ps   &   |- ch   &   |- th   &   |- (((ph /\ ps) /\ (ch /\ th)) -> ta)   =>   |- ta
Theorem	mpan2d 655	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
|- (ph -> ch)   &   |- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> (ps -> th))
Theorem	mpand 656	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
|- (ph -> ps)   &   |- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> (ch -> th))
Theorem	mpani 657	An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
|- ps   &   |- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> (ch -> th))
Theorem	mpan2i 658	An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
|- ch   &   |- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> (ps -> th))
Theorem	mp2ani 659	An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.)
|- ps   &   |- ch   &   |- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> th)
Theorem	mp2and 660	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
|- (ph -> ps)   &   |- (ph -> ch)   &   |- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> th)
Theorem	mpanl1 661	An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
|- ph   &   |- (((ph /\ ps) /\ ch) -> th)   =>   |- ((ps /\ ch) -> th)
Theorem	mpanl2 662	An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- ps   &   |- (((ph /\ ps) /\ ch) -> th)   =>   |- ((ph /\ ch) -> th)
Theorem	mpanl12 663	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
|- ph   &   |- ps   &   |- (((ph /\ ps) /\ ch) -> th)   =>   |- (ch -> th)
Theorem	mpanr1 664	An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- ps   &   |- ((ph /\ (ps /\ ch)) -> th)   =>   |- ((ph /\ ch) -> th)
Theorem	mpanr2 665	An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
|- ch   &   |- ((ph /\ (ps /\ ch)) -> th)   =>   |- ((ph /\ ps) -> th)
Theorem	mpanr12 666	An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
|- ps   &   |- ch   &   |- ((ph /\ (ps /\ ch)) -> th)   =>   |- (ph -> th)
Theorem	mpanlr1 667	An inference based on modus ponens. (Contributed by NM, 30-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
|- ps   &   |- (((ph /\ (ps /\ ch)) /\ th) -> ta)   =>   |- (((ph /\ ch) /\ th) -> ta)
Theorem	pm5.74da 668	Distribution of implication over biconditional (deduction rule). (Contributed by NM, 4-May-2007.)
|- ((ph /\ ps) -> (ch <-> th))   =>   |- (ph -> ((ps -> ch) <-> (ps -> th)))
Theorem	pm4.45 669	Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
|- (ph <-> (ph /\ (ph \/ ps)))
Theorem	imdistan 670	Distribution of implication with conjunction. (Contributed by NM, 31-May-1999.) (Proof shortened by Wolf Lammen, 6-Dec-2012.)
|- ((ph -> (ps -> ch)) <-> ((ph /\ ps) -> (ph /\ ch)))
Theorem	imdistani 671	Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)
|- (ph -> (ps -> ch))   =>   |- ((ph /\ ps) -> (ph /\ ch))
Theorem	imdistanri 672	Distribution of implication with conjunction. (Contributed by NM, 8-Jan-2002.)
|- (ph -> (ps -> ch))   =>   |- ((ps /\ ph) -> (ch /\ ph))
Theorem	imdistand 673	Distribution of implication with conjunction (deduction rule). (Contributed by NM, 27-Aug-2004.)
|- (ph -> (ps -> (ch -> th)))   =>   |- (ph -> ((ps /\ ch) -> (ps /\ th)))
Theorem	imdistanda 674	Distribution of implication with conjunction (deduction version with conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.)
|- ((ph /\ ps) -> (ch -> th))   =>   |- (ph -> ((ps /\ ch) -> (ps /\ th)))
Theorem	anbi2i 675	Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
|- (ph <-> ps)   =>   |- ((ch /\ ph) <-> (ch /\ ps))
Theorem	anbi1i 676	Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
|- (ph <-> ps)   =>   |- ((ph /\ ch) <-> (ps /\ ch))
Theorem	anbi2ci 677	Variant of anbi2i 675 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- (ph <-> ps)   =>   |- ((ph /\ ch) <-> (ch /\ ps))
Theorem	anbi12i 678	Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.)
|- (ph <-> ps)   &   |- (ch <-> th)   =>   |- ((ph /\ ch) <-> (ps /\ th))
Theorem	anbi12ci 679	Variant of anbi12i 678 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph <-> ps)   &   |- (ch <-> th)   =>   |- ((ph /\ ch) <-> (th /\ ps))
Theorem	sylan9bb 680	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
|- (ph -> (ps <-> ch))   &   |- (th -> (ch <-> ta))   =>   |- ((ph /\ th) -> (ps <-> ta))
Theorem	sylan9bbr 681	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
|- (ph -> (ps <-> ch))   &   |- (th -> (ch <-> ta))   =>   |- ((th /\ ph) -> (ps <-> ta))
Theorem	orbi2d 682	Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> ((th \/ ps) <-> (th \/ ch)))
Theorem	orbi1d 683	Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> ((ps \/ th) <-> (ch \/ th)))
Theorem	anbi2d 684	Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> ((th /\ ps) <-> (th /\ ch)))
Theorem	anbi1d 685	Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> ((ps /\ th) <-> (ch /\ th)))
Theorem	orbi1 686	Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- ((ph <-> ps) -> ((ph \/ ch) <-> (ps \/ ch)))
Theorem	anbi1 687	Introduce a right conjunct to both sides of a logical equivalence. Theorem *4.36 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- ((ph <-> ps) -> ((ph /\ ch) <-> (ps /\ ch)))
Theorem	anbi2 688	Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 16-Nov-2013.)
|- ((ph <-> ps) -> ((ch /\ ph) <-> (ch /\ ps)))
Theorem	bitr 689	Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
|- (((ph <-> ps) /\ (ps <-> ch)) -> (ph <-> ch))
Theorem	orbi12d 690	Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ta))   =>   |- (ph -> ((ps \/ th) <-> (ch \/ ta)))
Theorem	anbi12d 691	Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ta))   =>   |- (ph -> ((ps /\ th) <-> (ch /\ ta)))
Theorem	pm5.3 692	Theorem *5.3 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- (((ph /\ ps) -> ch) <-> ((ph /\ ps) -> (ph /\ ch)))
Theorem	pm5.61 693	Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.)
|- (((ph \/ ps) /\ -. ps) <-> (ph /\ -. ps))
Theorem	adantll 694	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|- ((ph /\ ps) -> ch)   =>   |- (((th /\ ph) /\ ps) -> ch)
Theorem	adantlr 695	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|- ((ph /\ ps) -> ch)   =>   |- (((ph /\ th) /\ ps) -> ch)
Theorem	adantrl 696	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|- ((ph /\ ps) -> ch)   =>   |- ((ph /\ (th /\ ps)) -> ch)
Theorem	adantrr 697	Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|- ((ph /\ ps) -> ch)   =>   |- ((ph /\ (ps /\ th)) -> ch)
Theorem	adantlll 698	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)
|- (((ph /\ ps) /\ ch) -> th)   =>   |- ((((ta /\ ph) /\ ps) /\ ch) -> th)
Theorem	adantllr 699	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
|- (((ph /\ ps) /\ ch) -> th)   =>   |- ((((ph /\ ta) /\ ps) /\ ch) -> th)
Theorem	adantlrl 700	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
|- (((ph /\ ps) /\ ch) -> th)   =>   |- (((ph /\ (ta /\ ps)) /\ ch) -> th)