P. 8 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 701-800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sylancom 701	Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ch /\ ps ) -> th )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	mpdan 702	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 703	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	mpidan 704	A deduction which "stacks" a hypothesis. (Contributed by Stanislas Polu, 9-Mar-2020.) (Proof shortened by Wolf Lammen, 28-Mar-2021.)
|- ( ph -> ch )   &    |- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	hypstkdOLD 705	Obsolete proof of mpidan 704 as of 28-Mar-2021. (Contributed by Stanislas Polu, 9-Mar-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> ch )   &    |- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	mpan 706	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 707	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 708	An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)
|- ph   &    |- ps   &    |- ( ( ph /\ ps ) -> ch )   =>    |- ch
Theorem	mp4an 709	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 710	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
|- ( ph -> ch )   &    |- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ph -> ( ps -> th ) )
Theorem	mpand 711	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 712	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 713	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 714	An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.)
|- ps   &    |- ch   &    |- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ph -> th )
Theorem	mp2and 715	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ph -> th )
Theorem	mpanl1 716	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 717	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 718	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
|- ph   &    |- ps   &    |- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ch -> th )
Theorem	mpanr1 719	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 720	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 721	An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
|- ps   &    |- ch   &    |- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ph -> th )
Theorem	mpanlr1 722	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 723	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 724	Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
|- ( ph <-> ( ph /\ ( ph \/ ps ) ) )
Theorem	imdistan 725	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 726	Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ( ph /\ ps ) -> ( ph /\ ch ) )
Theorem	imdistanri 727	Distribution of implication with conjunction. (Contributed by NM, 8-Jan-2002.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ( ps /\ ph ) -> ( ch /\ ph ) )
Theorem	imdistand 728	Distribution of implication with conjunction (deduction rule). (Contributed by NM, 27-Aug-2004.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ph -> ( ( ps /\ ch ) -> ( ps /\ th ) ) )
Theorem	imdistanda 729	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 730	Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
|- ( ph <-> ps )   =>    |- ( ( ch /\ ph ) <-> ( ch /\ ps ) )
Theorem	anbi1i 731	Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
|- ( ph <-> ps )   =>    |- ( ( ph /\ ch ) <-> ( ps /\ ch ) )
Theorem	anbi2ci 732	Variant of anbi2i 730 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 733	Conjoin both sides of two equivalences. (Contributed by NM, 12-Mar-1993.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   =>    |- ( ( ph /\ ch ) <-> ( ps /\ th ) )
Theorem	anbi12ci 734	Variant of anbi12i 733 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   =>    |- ( ( ph /\ ch ) <-> ( th /\ ps ) )
Theorem	syldanl 735	A syllogism deduction with conjoined antecedents. (Contributed by Jeff Madsen, 20-Jun-2011.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ( ph /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ph /\ ps ) /\ th ) -> ta )
Theorem	sylan9bb 736	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( th -> ( ch <-> ta ) )   =>    |- ( ( ph /\ th ) -> ( ps <-> ta ) )
Theorem	sylan9bbr 737	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( th -> ( ch <-> ta ) )   =>    |- ( ( th /\ ph ) -> ( ps <-> ta ) )
Theorem	orbi2d 738	Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( th \/ ps ) <-> ( th \/ ch ) ) )
Theorem	orbi1d 739	Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ th ) ) )
Theorem	anbi2d 740	Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( th /\ ps ) <-> ( th /\ ch ) ) )
Theorem	anbi1d 741	Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )
Theorem	orbi1 742	Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph <-> ps ) -> ( ( ph \/ ch ) <-> ( ps \/ ch ) ) )
Theorem	anbi1 743	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 744	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 745	Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph <-> ps ) /\ ( ps <-> ch ) ) -> ( ph <-> ch ) )
Theorem	orbi12d 746	Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 21-Jun-1993.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   =>    |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )
Theorem	anbi12d 747	Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 26-May-1993.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   =>    |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ ta ) ) )
Theorem	pm5.3 748	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 749	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 750	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 751	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 752	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 753	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 754	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 755	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 756	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	adantlrr 757	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 /\ ( ps /\ ta ) ) /\ ch ) -> th )
Theorem	adantrll 758	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	adantrlr 759	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 /\ ( ( ps /\ ta ) /\ ch ) ) -> th )
Theorem	adantrrl 760	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 /\ ( ps /\ ( ta /\ ch ) ) ) -> th )
Theorem	adantrrr 761	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 /\ ( ps /\ ( ch /\ ta ) ) ) -> th )
Theorem	ad2antrr 762	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
|- ( ph -> ps )   =>    |- ( ( ( ph /\ ch ) /\ th ) -> ps )
Theorem	ad2antlr 763	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
|- ( ph -> ps )   =>    |- ( ( ( ch /\ ph ) /\ th ) -> ps )
Theorem	ad2antrl 764	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
|- ( ph -> ps )   =>    |- ( ( ch /\ ( ph /\ th ) ) -> ps )
Theorem	ad2antll 765	Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
|- ( ph -> ps )   =>    |- ( ( ch /\ ( th /\ ph ) ) -> ps )
Theorem	ad3antrrr 766	Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)
|- ( ph -> ps )   =>    |- ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) -> ps )
Theorem	ad3antlr 767	Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) -> ps )
Theorem	ad4antr 768	Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )
Theorem	ad4antlr 769	Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) /\ et ) -> ps )
Theorem	ad5antr 770	Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ps )
Theorem	ad5antlr 771	Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ps )
Theorem	ad6antr 772	Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> ps )
Theorem	ad6antlr 773	Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> ps )
Theorem	ad7antr 774	Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) -> ps )
Theorem	ad7antlr 775	Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) -> ps )
Theorem	ad8antr 776	Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) -> ps )
Theorem	ad8antlr 777	Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) -> ps )
Theorem	ad9antr 778	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 779	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 780	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 781	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 782	Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( th /\ ph ) /\ ( ta /\ ps ) ) -> ch )
Theorem	ad2ant2r 783	Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ph /\ th ) /\ ( ps /\ ta ) ) -> ch )
Theorem	ad2ant2lr 784	Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( th /\ ph ) /\ ( ps /\ ta ) ) -> ch )
Theorem	ad2ant2rl 785	Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ph /\ th ) /\ ( ta /\ ps ) ) -> ch )
Theorem	adantl3r 786	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( ( ( ph /\ rh ) /\ mu ) /\ la ) -> ka )   =>    |- ( ( ( ( ( ph /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )
Theorem	adantl4r 787	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	adantl5r 788	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 789	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 790	Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
|- ( ( ( ph /\ ps ) /\ ch ) -> ph )
Theorem	simplld 791	Deduction form of simpll 790, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ( ( ps /\ ch ) /\ th ) )   =>    |- ( ph -> ps )
Theorem	simplr 792	Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)
|- ( ( ( ph /\ ps ) /\ ch ) -> ps )
Theorem	simplrd 793	Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ( ( ps /\ ch ) /\ th ) )   =>    |- ( ph -> ch )
Theorem	simprl 794	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
|- ( ( ph /\ ( ps /\ ch ) ) -> ps )
Theorem	simprld 795	Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ( ps /\ ( ch /\ th ) ) )   =>    |- ( ph -> ch )
Theorem	simprr 796	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
|- ( ( ph /\ ( ps /\ ch ) ) -> ch )
Theorem	simprrd 797	Deduction form of simprr 796, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ( ps /\ ( ch /\ th ) ) )   =>    |- ( ph -> th )
Theorem	simplll 798	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ph )
Theorem	simpllr 799	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )
Theorem	simplrl 800	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )