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	simpllr 501	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )
Theorem	simplrl 502	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )
Theorem	simplrr 503	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ch )
Theorem	simprll 504	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ps )
Theorem	simprlr 505	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ch )
Theorem	simprrl 506	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ch )
Theorem	simprrr 507	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> th )
Theorem	simp-4l 508	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ph )
Theorem	simp-4r 509	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ps )
Theorem	simp-5l 510	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) -> ph )
Theorem	simp-5r 511	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )
Theorem	simp-6l 512	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ph )
Theorem	simp-6r 513	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ps )
Theorem	simp-7l 514	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> ph )
Theorem	simp-7r 515	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> ps )
Theorem	simp-8l 516	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) -> ph )
Theorem	simp-8r 517	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) -> ps )
Theorem	simp-9l 518	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 519	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 520	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 521	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 522	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 523	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 524	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	abai 525	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 526	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 527	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 528	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 529	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 530	Swap two conjuncts in antecedent. The label suffix "s" means that an12 526 is combined with syl 14 (or a variant). (Contributed by NM, 13-Mar-1996.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ps /\ ( ph /\ ch ) ) -> th )
Theorem	ancom2s 531	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 532	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ch /\ ( ps /\ ph ) ) -> th )
Theorem	an32s 533	Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ph /\ ch ) /\ ps ) -> th )
Theorem	ancom1s 534	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 535	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ch /\ ps ) /\ ph ) -> th )
Theorem	anass1rs 536	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 537	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 538	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 539	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 540	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 541	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 542	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.)
|- ( ( ( ps /\ ph ) /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabss5 543	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 544	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 545	Absorption of antecedent into conjunction. (Contributed by NM, 14-Aug-2000.)
|- ( ph -> ( ( ps /\ ph ) -> ch ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabsi7 546	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 547	Absorption of antecedent into conjunction. (Contributed by NM, 26-Sep-1999.)
|- ( ps -> ( ( ps /\ ph ) -> ch ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabss7 548	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 549	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 550	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 551	Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch ) /\ ( ps /\ th ) ) )
Theorem	an42 552	Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch ) /\ ( th /\ ps ) ) )
Theorem	an4s 553	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
Theorem	an42s 554	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ( ph /\ ch ) /\ ( th /\ ps ) ) -> ta )
Theorem	anandi 555	Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
|- ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
Theorem	anandir 556	Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ph /\ ch ) /\ ( ps /\ ch ) ) )
Theorem	anandis 557	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
|- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) -> ta )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> ta )
Theorem	anandirs 558	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
|- ( ( ( ph /\ ch ) /\ ( ps /\ ch ) ) -> ta )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> ta )
Theorem	syl2an2 559	syl2an 283 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 560	syl2anr 284 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 561	Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ ch ) -> ps )   =>    |- ( ph -> ( ps <-> ch ) )
Theorem	pm3.45 562	Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ps ) -> ( ( ph /\ ch ) -> ( ps /\ ch ) ) )
Theorem	im2anan9 563	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 564	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 565	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 566	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 567	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 568	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 569	Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) <-> ( ph -> ( ps /\ ch ) ) )
Theorem	pm4.38 570	Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph <-> ch ) /\ ( ps <-> th ) ) -> ( ( ph /\ ps ) <-> ( ch /\ th ) ) )
Theorem	bi2anan9 571	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 572	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 573	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 574	Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph /\ ( ps -> ch ) ) <-> ( ph /\ ( ( ph /\ ps ) -> ch ) ) )
Theorem	pm5.36 575	Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph /\ ( ph <-> ps ) ) <-> ( ps /\ ( ph <-> ps ) ) )
Theorem	bianabs 576	Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.)
|- ( ph -> ( ps <-> ( ph /\ ch ) ) )   =>    |- ( ph -> ( ps <-> ch ) )
1.2.5  Logical negation (intuitionistic)
Axiom	ax-in1 577	'Not' introduction. One of the axioms of propositional logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- ( ( ph -> -. ph ) -> -. ph )
Axiom	ax-in2 578	'Not' elimination. One of the axioms of propositional logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- ( -. ph -> ( ph -> ps ) )
Theorem	pm2.01 579	Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100. This is valid intuitionistically (in the terminology of Section 1.2 of [Bauer] p. 482 it is a proof of negation not a proof by contradiction); compare with pm2.18dc 784 which only holds for some propositions. (Contributed by Mario Carneiro, 12-May-2015.)
|- ( ( ph -> -. ph ) -> -. ph )
Theorem	pm2.21 580	From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. (Contributed by Mario Carneiro, 12-May-2015.)
|- ( -. ph -> ( ph -> ps ) )
Theorem	pm2.01d 581	Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ph -> ( ps -> -. ps ) )   =>    |- ( ph -> -. ps )
Theorem	pm2.21d 582	A contradiction implies anything. Deduction from pm2.21 580. (Contributed by NM, 10-Feb-1996.)
|- ( ph -> -. ps )   =>    |- ( ph -> ( ps -> ch ) )
Theorem	pm2.21dd 583	A contradiction implies anything. Deduction from pm2.21 580. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ph -> ps )   &    |- ( ph -> -. ps )   =>    |- ( ph -> ch )
Theorem	pm2.24 584	Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
|- ( ph -> ( -. ph -> ps ) )
Theorem	pm2.24d 585	Deduction version of pm2.24 584. (Contributed by NM, 30-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ph -> ps )   =>    |- ( ph -> ( -. ps -> ch ) )
Theorem	pm2.24i 586	Inference version of pm2.24 584. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ph   =>    |- ( -. ph -> ps )
Theorem	con2d 587	A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised by NM, 12-Feb-2013.)
|- ( ph -> ( ps -> -. ch ) )   =>    |- ( ph -> ( ch -> -. ps ) )
Theorem	mt2d 588	Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
|- ( ph -> ch )   &    |- ( ph -> ( ps -> -. ch ) )   =>    |- ( ph -> -. ps )
Theorem	nsyl3 589	A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) (Revised by NM, 13-Jun-2013.)
|- ( ph -> -. ps )   &    |- ( ch -> ps )   =>    |- ( ch -> -. ph )
Theorem	con2i 590	A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.)
|- ( ph -> -. ps )   =>    |- ( ps -> -. ph )
Theorem	nsyl 591	A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
|- ( ph -> -. ps )   &    |- ( ch -> ps )   =>    |- ( ph -> -. ch )
Theorem	notnot 592	Double negation introduction. Theorem *2.12 of [WhiteheadRussell] p. 101. This one holds for all propositions, but its converse only holds for decidable propositions (see notnotrdc 785). (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
|- ( ph -> -. -. ph )
Theorem	notnotd 593	Deduction associated with notnot 592 and notnoti 607. (Contributed by Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf Lammen, 27-Mar-2021.)
|- ( ph -> ps )   =>    |- ( ph -> -. -. ps )
Theorem	con3d 594	A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( -. ch -> -. ps ) )
Theorem	con3i 595	A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)
|- ( ph -> ps )   =>    |- ( -. ps -> -. ph )
Theorem	con3rr3 596	Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( -. ch -> ( ph -> -. ps ) )
Theorem	con3dimp 597	Variant of con3d 594 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ( ph /\ -. ch ) -> -. ps )
Theorem	pm2.01da 598	Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ( ph /\ ps ) -> -. ps )   =>    |- ( ph -> -. ps )
Theorem	pm3.2im 599	In classical logic, this is just a restatement of pm3.2 137. In intuitionistic logic, it still holds, but is weaker than pm3.2. (Contributed by Mario Carneiro, 12-May-2015.)
|- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
Theorem	expi 600	An exportation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.)
|- ( -. ( ph -> -. ps ) -> ch )   =>    |- ( ph -> ( ps -> ch ) )