P. 7 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 601-700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	exp53 601	An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ( ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) /\ ta ) -> et )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )
Theorem	expl 602	Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ph -> ( ( ps /\ ch ) -> th ) )
Theorem	impr 603	Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ( ( ph /\ ps ) -> ( ch -> th ) )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> th )
Theorem	impl 604	Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> th )
Theorem	impac 605	Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ( ph /\ ps ) -> ( ch /\ ps ) )
Theorem	exbiri 606	Inference form of exbir 1371. This proof is exbiriVD 28675 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 607	Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	simplbda 608	Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	simplbi2 609	Deduction eliminating a conjunct. Automatically derived from simplbi2VD 28667. (Contributed by Alan Sare, 31-Dec-2011.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ch -> ph ) )
Theorem	dfbi2 610	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 611	Definition df-bi 178 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 612	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 613	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 614	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 615	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 616	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 617	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 618	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 619	Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ( ph /\ ps ) <-> ( ph /\ ch ) )
Theorem	pm5.32ri 620	Distribution of implication over biconditional (inference rule). (Contributed by NM, 12-Mar-1995.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ( ps /\ ph ) <-> ( ch /\ ph ) )
Theorem	pm5.32d 621	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 622	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 623	Distribution of implication over biconditional (deduction rule). (Contributed by NM, 9-Dec-2006.)
|- ( ( ph /\ ps ) -> ( ch <-> th ) )   =>    |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )
Theorem	biadan2 624	Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.)
|- ( ph -> ps )   &    |- ( ps -> ( ph <-> ch ) )   =>    |- ( ph <-> ( ps /\ ch ) )
Theorem	pm4.24 625	Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
|- ( ph <-> ( ph /\ ph ) )
Theorem	anidm 626	Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)
|- ( ( ph /\ ph ) <-> ph )
Theorem	anidms 627	Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)
|- ( ( ph /\ ph ) -> ps )   =>    |- ( ph -> ps )
Theorem	anidmdbi 628	Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.)
|- ( ( ph -> ( ps /\ ps ) ) <-> ( ph -> ps ) )
Theorem	anasss 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	anassrs 630	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 631	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 632	A syllogism inference. (Contributed by NM, 10-Mar-2005.)
|- ( ph -> ps )   &    |- ( ( ( ps /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ph /\ ch ) /\ th ) -> ta )
Theorem	sylanl2 633	A syllogism inference. (Contributed by NM, 1-Jan-2005.)
|- ( ph -> ch )   &    |- ( ( ( ps /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ps /\ ph ) /\ th ) -> ta )
Theorem	sylanr1 634	A syllogism inference. (Contributed by NM, 9-Apr-2005.)
|- ( ph -> ch )   &    |- ( ( ps /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ps /\ ( ph /\ th ) ) -> ta )
Theorem	sylanr2 635	A syllogism inference. (Contributed by NM, 9-Apr-2005.)
|- ( ph -> th )   &    |- ( ( ps /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ps /\ ( ch /\ ph ) ) -> ta )
Theorem	sylani 636	A syllogism inference. (Contributed by NM, 2-May-1996.)
|- ( ph -> ch )   &    |- ( ps -> ( ( ch /\ th ) -> ta ) )   =>    |- ( ps -> ( ( ph /\ th ) -> ta ) )
Theorem	sylan2i 637	A syllogism inference. (Contributed by NM, 1-Aug-1994.)
|- ( ph -> th )   &    |- ( ps -> ( ( ch /\ th ) -> ta ) )   =>    |- ( ps -> ( ( ch /\ ph ) -> ta ) )
Theorem	syl2ani 638	A syllogism inference. (Contributed by NM, 3-Aug-1999.)
|- ( ph -> ch )   &    |- ( et -> th )   &    |- ( ps -> ( ( ch /\ th ) -> ta ) )   =>    |- ( ps -> ( ( ph /\ et ) -> ta ) )
Theorem	sylan9 639	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 640	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ps -> ch ) )   &    |- ( th -> ( ch -> ta ) )   =>    |- ( ( th /\ ph ) -> ( ps -> ta ) )
Theorem	mtand 641	A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
|- ( ph -> -. ch )   &    |- ( ( ph /\ ps ) -> ch )   =>    |- ( ph -> -. ps )
Theorem	mtord 642	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 643	Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	sylancl 644	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ph -> ps )   &    |- ch   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	sylancr 645	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ps   &    |- ( ph -> ch )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	sylanbrc 646	Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( th <-> ( ps /\ ch ) )   =>    |- ( ph -> th )
Theorem	sylancb 647	A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)
|- ( ph <-> ps )   &    |- ( ph <-> ch )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	sylancbr 648	A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)
|- ( ps <-> ph )   &    |- ( ch <-> ph )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	sylancom 649	Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ch /\ ps ) -> th )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	mpdan 650	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 651	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 652	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 653	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 654	An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)
|- ph   &    |- ps   &    |- ( ( ph /\ ps ) -> ch )   =>    |- ch
Theorem	mp4an 655	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 656	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
|- ( ph -> ch )   &    |- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ph -> ( ps -> th ) )
Theorem	mpand 657	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 658	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 659	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 660	An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.)
|- ps   &    |- ch   &    |- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ph -> th )
Theorem	mp2and 661	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ph -> th )
Theorem	mpanl1 662	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 663	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 664	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
|- ph   &    |- ps   &    |- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ch -> th )
Theorem	mpanr1 665	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 666	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 667	An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
|- ps   &    |- ch   &    |- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ph -> th )
Theorem	mpanlr1 668	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 669	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 670	Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
|- ( ph <-> ( ph /\ ( ph \/ ps ) ) )
Theorem	imdistan 671	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 672	Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ( ph /\ ps ) -> ( ph /\ ch ) )
Theorem	imdistanri 673	Distribution of implication with conjunction. (Contributed by NM, 8-Jan-2002.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ( ps /\ ph ) -> ( ch /\ ph ) )
Theorem	imdistand 674	Distribution of implication with conjunction (deduction rule). (Contributed by NM, 27-Aug-2004.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ph -> ( ( ps /\ ch ) -> ( ps /\ th ) ) )
Theorem	imdistanda 675	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 676	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 677	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 678	Variant of anbi2i 676 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 679	Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   =>    |- ( ( ph /\ ch ) <-> ( ps /\ th ) )
Theorem	anbi12ci 680	Variant of anbi12i 679 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   =>    |- ( ( ph /\ ch ) <-> ( th /\ ps ) )
Theorem	sylan9bb 681	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( th -> ( ch <-> ta ) )   =>    |- ( ( ph /\ th ) -> ( ps <-> ta ) )
Theorem	sylan9bbr 682	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( th -> ( ch <-> ta ) )   =>    |- ( ( th /\ ph ) -> ( ps <-> ta ) )
Theorem	orbi2d 683	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 684	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 685	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 686	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 687	Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph <-> ps ) -> ( ( ph \/ ch ) <-> ( ps \/ ch ) ) )
Theorem	anbi1 688	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 689	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 690	Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph <-> ps ) /\ ( ps <-> ch ) ) -> ( ph <-> ch ) )
Theorem	orbi12d 691	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 692	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 693	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 694	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 695	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 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	adantrl 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 /\ ( th /\ ps ) ) -> ch )
Theorem	adantrr 698	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 699	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 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 )