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	pm4.87 501	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 502	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 503	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 504	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 505	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 506	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 507	Swap two conjuncts in antecedent. The label suffix "s" means that an12 503 is combined with syl 14 (or a variant). (Contributed by NM, 13-Mar-1996.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ps /\ ( ph /\ ch ) ) -> th )
Theorem	ancom2s 508	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 509	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ch /\ ( ps /\ ph ) ) -> th )
Theorem	an32s 510	Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ph /\ ch ) /\ ps ) -> th )
Theorem	ancom1s 511	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 512	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ch /\ ps ) /\ ph ) -> th )
Theorem	anass1rs 513	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 514	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 515	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 516	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 517	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 518	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 519	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.)
|- ( ( ( ps /\ ph ) /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabss5 520	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 521	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 522	Absorption of antecedent into conjunction. (Contributed by NM, 14-Aug-2000.)
|- ( ph -> ( ( ps /\ ph ) -> ch ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabsi7 523	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 524	Absorption of antecedent into conjunction. (Contributed by NM, 26-Sep-1999.)
|- ( ps -> ( ( ps /\ ph ) -> ch ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabss7 525	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 526	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 527	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 528	Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch ) /\ ( ps /\ th ) ) )
Theorem	an42 529	Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch ) /\ ( th /\ ps ) ) )
Theorem	an4s 530	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
Theorem	an42s 531	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ( ph /\ ch ) /\ ( th /\ ps ) ) -> ta )
Theorem	anandi 532	Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
|- ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
Theorem	anandir 533	Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ph /\ ch ) /\ ( ps /\ ch ) ) )
Theorem	anandis 534	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
|- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) -> ta )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> ta )
Theorem	anandirs 535	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
|- ( ( ( ph /\ ch ) /\ ( ps /\ ch ) ) -> ta )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> ta )
Theorem	syl2an2 536	syl2an 277 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 537	syl2anr 278 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 538	Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ ch ) -> ps )   =>    |- ( ph -> ( ps <-> ch ) )
Theorem	pm3.45 539	Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ps ) -> ( ( ph /\ ch ) -> ( ps /\ ch ) ) )
Theorem	im2anan9 540	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 541	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 542	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 543	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 544	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 545	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 546	Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) <-> ( ph -> ( ps /\ ch ) ) )
Theorem	pm4.38 547	Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph <-> ch ) /\ ( ps <-> th ) ) -> ( ( ph /\ ps ) <-> ( ch /\ th ) ) )
Theorem	bi2anan9 548	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 549	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 550	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 551	Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph /\ ( ps -> ch ) ) <-> ( ph /\ ( ( ph /\ ps ) -> ch ) ) )
Theorem	pm5.36 552	Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph /\ ( ph <-> ps ) ) <-> ( ps /\ ( ph <-> ps ) ) )
Theorem	bianabs 553	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 554	'Not' introduction. One of the axioms of propositional logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- ( ( ph -> -. ph ) -> -. ph )
Axiom	ax-in2 555	'Not' elimination. One of the axioms of propositional logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- ( -. ph -> ( ph -> ps ) )
Theorem	pm2.01 556	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 761 which only holds for some propositions. (Contributed by Mario Carneiro, 12-May-2015.)
|- ( ( ph -> -. ph ) -> -. ph )
Theorem	pm2.21 557	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 558	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 559	A contradiction implies anything. Deduction from pm2.21 557. (Contributed by NM, 10-Feb-1996.)
|- ( ph -> -. ps )   =>    |- ( ph -> ( ps -> ch ) )
Theorem	pm2.21dd 560	A contradiction implies anything. Deduction from pm2.21 557. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ph -> ps )   &    |- ( ph -> -. ps )   =>    |- ( ph -> ch )
Theorem	pm2.24 561	Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
|- ( ph -> ( -. ph -> ps ) )
Theorem	pm2.24d 562	Deduction version of pm2.24 561. (Contributed by NM, 30-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ph -> ps )   =>    |- ( ph -> ( -. ps -> ch ) )
Theorem	pm2.24i 563	Inference version of pm2.24 561. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ph   =>    |- ( -. ph -> ps )
Theorem	con2d 564	A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised by NM, 12-Feb-2013.)
|- ( ph -> ( ps -> -. ch ) )   =>    |- ( ph -> ( ch -> -. ps ) )
Theorem	mt2d 565	Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
|- ( ph -> ch )   &    |- ( ph -> ( ps -> -. ch ) )   =>    |- ( ph -> -. ps )
Theorem	nsyl3 566	A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) (Revised by NM, 13-Jun-2013.)
|- ( ph -> -. ps )   &    |- ( ch -> ps )   =>    |- ( ch -> -. ph )
Theorem	con2i 567	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 568	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 569	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 762). (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
|- ( ph -> -. -. ph )
Theorem	notnotd 570	Deduction associated with notnot 569 and notnoti 584. (Contributed by Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf Lammen, 27-Mar-2021.)
|- ( ph -> ps )   =>    |- ( ph -> -. -. ps )
Theorem	con3d 571	A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( -. ch -> -. ps ) )
Theorem	con3i 572	A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)
|- ( ph -> ps )   =>    |- ( -. ps -> -. ph )
Theorem	con3rr3 573	Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( -. ch -> ( ph -> -. ps ) )
Theorem	con3dimp 574	Variant of con3d 571 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ( ph /\ -. ch ) -> -. ps )
Theorem	pm2.01da 575	Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ( ph /\ ps ) -> -. ps )   =>    |- ( ph -> -. ps )
Theorem	pm3.2im 576	In classical logic, this is just a restatement of pm3.2 130. 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 577	An exportation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.)
|- ( -. ( ph -> -. ps ) -> ch )   =>    |- ( ph -> ( ps -> ch ) )
Theorem	pm2.65i 578	Inference rule for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
|- ( ph -> ps )   &    |- ( ph -> -. ps )   =>    |- -. ph
Theorem	mt2 579	A rule similar to modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.)
|- ps   &    |- ( ph -> -. ps )   =>    |- -. ph
Theorem	biijust 580	Theorem used to justify definition of intuitionistic biconditional df-bi 114. (Contributed by NM, 24-Nov-2017.)
|- ( ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) /\ ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) )
Theorem	con3 581	Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Feb-2013.)
|- ( ( ph -> ps ) -> ( -. ps -> -. ph ) )
Theorem	con2 582	Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
|- ( ( ph -> -. ps ) -> ( ps -> -. ph ) )
Theorem	mt2i 583	Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
|- ch   &    |- ( ph -> ( ps -> -. ch ) )   =>    |- ( ph -> -. ps )
Theorem	notnoti 584	Infer double negation. (Contributed by NM, 27-Feb-2008.)
|- ph   =>    |- -. -. ph
Theorem	pm2.21i 585	A contradiction implies anything. Inference from pm2.21 557. (Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- -. ph   =>    |- ( ph -> ps )
Theorem	pm2.24ii 586	A contradiction implies anything. Inference from pm2.24 561. (Contributed by NM, 27-Feb-2008.)
|- ph   &    |- -. ph   =>    |- ps
Theorem	nsyld 587	A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.)
|- ( ph -> ( ps -> -. ch ) )   &    |- ( ph -> ( ta -> ch ) )   =>    |- ( ph -> ( ps -> -. ta ) )
Theorem	nsyli 588	A negated syllogism inference. (Contributed by NM, 3-May-1994.)
|- ( ph -> ( ps -> ch ) )   &    |- ( th -> -. ch )   =>    |- ( ph -> ( th -> -. ps ) )
Theorem	mth8 589	Theorem 8 of [Margaris] p. 60. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
|- ( ph -> ( -. ps -> -. ( ph -> ps ) ) )
Theorem	jc 590	Inference joining the consequents of two premises. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   &    |- ( ph -> ch )   =>    |- ( ph -> -. ( ps -> -. ch ) )
Theorem	pm2.51 591	Theorem *2.51 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
|- ( -. ( ph -> ps ) -> ( ph -> -. ps ) )
Theorem	pm2.52 592	Theorem *2.52 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( -. ( ph -> ps ) -> ( -. ph -> -. ps ) )
Theorem	expt 593	Exportation theorem expressed with primitive connectives. (Contributed by NM, 5-Aug-1993.)
|- ( ( -. ( ph -> -. ps ) -> ch ) -> ( ph -> ( ps -> ch ) ) )
Theorem	jarl 594	Elimination of a nested antecedent. (Contributed by Wolf Lammen, 10-May-2013.)
|- ( ( ( ph -> ps ) -> ch ) -> ( -. ph -> ch ) )
Theorem	pm2.65 595	Theorem *2.65 of [WhiteheadRussell] p. 107. Proof by contradiction. Proofs, such as this one, which assume a proposition, here ph, derive a contradiction, and therefore conclude -. ph, are valid intuitionistically (and can be called "proof of negation", for example by Section 1.2 of [Bauer] p. 482). By contrast, proofs which assume -. ph, derive a contradiction, and conclude ph, such as condandc 786, are only valid for decidable propositions. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Mar-2013.)
|- ( ( ph -> ps ) -> ( ( ph -> -. ps ) -> -. ph ) )
Theorem	pm2.65d 596	Deduction rule for proof by contradiction. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ps -> -. ch ) )   =>    |- ( ph -> -. ps )
Theorem	pm2.65da 597	Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ ps ) -> -. ch )   =>    |- ( ph -> -. ps )
Theorem	mto 598	The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
|- -. ps   &    |- ( ph -> ps )   =>    |- -. ph
Theorem	mtod 599	Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
|- ( ph -> -. ch )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> -. ps )
Theorem	mtoi 600	Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
|- -. ch   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> -. ps )