P. 5 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 401-500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sylanl2 401	A syllogism inference. (Contributed by NM, 1-Jan-2005.)
|- ( ph -> ch )   &    |- ( ( ( ps /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ps /\ ph ) /\ th ) -> ta )
Theorem	sylanr1 402	A syllogism inference. (Contributed by NM, 9-Apr-2005.)
|- ( ph -> ch )   &    |- ( ( ps /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ps /\ ( ph /\ th ) ) -> ta )
Theorem	sylanr2 403	A syllogism inference. (Contributed by NM, 9-Apr-2005.)
|- ( ph -> th )   &    |- ( ( ps /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ps /\ ( ch /\ ph ) ) -> ta )
Theorem	sylani 404	A syllogism inference. (Contributed by NM, 2-May-1996.)
|- ( ph -> ch )   &    |- ( ps -> ( ( ch /\ th ) -> ta ) )   =>    |- ( ps -> ( ( ph /\ th ) -> ta ) )
Theorem	sylan2i 405	A syllogism inference. (Contributed by NM, 1-Aug-1994.)
|- ( ph -> th )   &    |- ( ps -> ( ( ch /\ th ) -> ta ) )   =>    |- ( ps -> ( ( ch /\ ph ) -> ta ) )
Theorem	syl2ani 406	A syllogism inference. (Contributed by NM, 3-Aug-1999.)
|- ( ph -> ch )   &    |- ( et -> th )   &    |- ( ps -> ( ( ch /\ th ) -> ta ) )   =>    |- ( ps -> ( ( ph /\ et ) -> ta ) )
Theorem	sylan9 407	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 408	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ( ps -> ch ) )   &    |- ( th -> ( ch -> ta ) )   =>    |- ( ( th /\ ph ) -> ( ps -> ta ) )
Theorem	syl2anc 409	Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	sylancl 410	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ph -> ps )   &    |- ch   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	sylancr 411	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ps   &    |- ( ph -> ch )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	sylanblc 412	Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.)
|- ( ph -> ps )   &    |- ch   &    |- ( ( ps /\ ch ) <-> th )   =>    |- ( ph -> th )
Theorem	sylanblrc 413	Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.)
|- ( ph -> ps )   &    |- ch   &    |- ( th <-> ( ps /\ ch ) )   =>    |- ( ph -> th )
Theorem	sylanbrc 414	Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( th <-> ( ps /\ ch ) )   =>    |- ( ph -> th )
Theorem	sylancb 415	A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)
|- ( ph <-> ps )   &    |- ( ph <-> ch )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	sylancbr 416	A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)
|- ( ps <-> ph )   &    |- ( ch <-> ph )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	sylancom 417	Syllogism inference with commutation of antecents. (Contributed by NM, 2-Jul-2008.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ch /\ ps ) -> th )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	mpdan 418	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 419	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 420	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	mpan 421	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 422	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 423	An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)
|- ph   &    |- ps   &    |- ( ( ph /\ ps ) -> ch )   =>    |- ch
Theorem	mp4an 424	An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2011.)
|- ph   &    |- ps   &    |- ch   &    |- th   &    |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )   =>    |- ta
Theorem	mpan2d 425	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
|- ( ph -> ch )   &    |- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ph -> ( ps -> th ) )
Theorem	mpand 426	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 427	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 428	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 429	An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.)
|- ps   &    |- ch   &    |- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ph -> th )
Theorem	mp2and 430	A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ph -> th )
Theorem	mpanl1 431	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 432	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 433	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
|- ph   &    |- ps   &    |- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ch -> th )
Theorem	mpanr1 434	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 435	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 436	An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
|- ps   &    |- ch   &    |- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ph -> th )
Theorem	mpanlr1 437	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	mpbirand 438	Detach truth from conjunction in biconditional. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> ch )   &    |- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ph -> ( ps <-> th ) )
Theorem	mpbiran2d 439	Detach truth from conjunction in biconditional. Deduction form. (Contributed by Peter Mazsa, 24-Sep-2022.)
|- ( ph -> th )   &    |- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ph -> ( ps <-> ch ) )
Theorem	pm5.74da 440	Distribution of implication over biconditional (deduction form). (Contributed by NM, 4-May-2007.)
|- ( ( ph /\ ps ) -> ( ch <-> th ) )   =>    |- ( ph -> ( ( ps -> ch ) <-> ( ps -> th ) ) )
Theorem	imdistan 441	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 442	Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ( ph /\ ps ) -> ( ph /\ ch ) )
Theorem	imdistanri 443	Distribution of implication with conjunction. (Contributed by NM, 8-Jan-2002.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ( ps /\ ph ) -> ( ch /\ ph ) )
Theorem	imdistand 444	Distribution of implication with conjunction (deduction form). (Contributed by NM, 27-Aug-2004.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ph -> ( ( ps /\ ch ) -> ( ps /\ th ) ) )
Theorem	imdistanda 445	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	pm5.32d 446	Distribution of implication over biconditional (deduction form). (Contributed by NM, 29-Oct-1996.) (Revised by NM, 31-Jan-2015.)
|- ( ph -> ( ps -> ( ch <-> th ) ) )   =>    |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )
Theorem	pm5.32rd 447	Distribution of implication over biconditional (deduction form). (Contributed by NM, 25-Dec-2004.)
|- ( ph -> ( ps -> ( ch <-> th ) ) )   =>    |- ( ph -> ( ( ch /\ ps ) <-> ( th /\ ps ) ) )
Theorem	pm5.32da 448	Distribution of implication over biconditional (deduction form). (Contributed by NM, 9-Dec-2006.)
|- ( ( ph /\ ps ) -> ( ch <-> th ) )   =>    |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )
Theorem	pm5.32 449	Distribution of implication over biconditional. Theorem *5.32 of [WhiteheadRussell] p. 125. (Contributed by NM, 1-Aug-1994.) (Revised by NM, 31-Jan-2015.)
|- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph /\ ps ) <-> ( ph /\ ch ) ) )
Theorem	pm5.32i 450	Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ( ph /\ ps ) <-> ( ph /\ ch ) )
Theorem	pm5.32ri 451	Distribution of implication over biconditional (inference form). (Contributed by NM, 12-Mar-1995.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ( ps /\ ph ) <-> ( ch /\ ph ) )
Theorem	biadan2 452	Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.)
|- ( ph -> ps )   &    |- ( ps -> ( ph <-> ch ) )   =>    |- ( ph <-> ( ps /\ ch ) )
Theorem	anbi2i 453	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 454	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 455	Variant of anbi2i 453 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 456	Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   =>    |- ( ( ph /\ ch ) <-> ( ps /\ th ) )
Theorem	anbi12ci 457	Variant of anbi12i 456 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   =>    |- ( ( ph /\ ch ) <-> ( th /\ ps ) )
Theorem	sylan9bb 458	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( th -> ( ch <-> ta ) )   =>    |- ( ( ph /\ th ) -> ( ps <-> ta ) )
Theorem	sylan9bbr 459	Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( th -> ( ch <-> ta ) )   =>    |- ( ( th /\ ph ) -> ( ps <-> ta ) )
Theorem	anbi2d 460	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 461	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	anbi1 462	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 463	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 464	Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph <-> ps ) /\ ( ps <-> ch ) ) -> ( ph <-> ch ) )
Theorem	anbi12d 465	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	mpan10 466	Modus ponens mixed with several conjunctions. (Contributed by Jim Kingdon, 7-Jan-2018.)
|- ( ( ( ( ph -> ps ) /\ ch ) /\ ph ) -> ( ps /\ ch ) )
Theorem	pm5.3 467	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	adantll 468	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 469	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 470	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 471	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 472	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 473	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 474	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 475	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 476	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 477	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 478	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 479	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 480	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 481	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 482	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
|- ( ph -> ps )   =>    |- ( ( ch /\ ( ph /\ th ) ) -> ps )
Theorem	ad2antll 483	Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
|- ( ph -> ps )   =>    |- ( ( ch /\ ( th /\ ph ) ) -> ps )
Theorem	ad3antrrr 484	Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)
|- ( ph -> ps )   =>    |- ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) -> ps )
Theorem	ad3antlr 485	Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) -> ps )
Theorem	ad4antr 486	Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )
Theorem	ad4antlr 487	Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) /\ et ) -> ps )
Theorem	ad5antr 488	Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ps )
Theorem	ad5antlr 489	Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- ( ph -> ps )   =>    |- ( ( ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ps )
Theorem	ad6antr 490	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 491	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 492	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 493	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 494	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 495	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 496	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 497	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 498	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 499	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 500	Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( th /\ ph ) /\ ( ta /\ ps ) ) -> ch )