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	simprl 501	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
|- ( ( ph /\ ( ps /\ ch ) ) -> ps )
Theorem	simprr 502	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
|- ( ( ph /\ ( ps /\ ch ) ) -> ch )
Theorem	simplll 503	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ph )
Theorem	simpllr 504	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )
Theorem	simplrl 505	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )
Theorem	simplrr 506	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ch )
Theorem	simprll 507	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ps )
Theorem	simprlr 508	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ch )
Theorem	simprrl 509	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ch )
Theorem	simprrr 510	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
|- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> th )
Theorem	simp-4l 511	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ph )
Theorem	simp-4r 512	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ps )
Theorem	simp-5l 513	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) -> ph )
Theorem	simp-5r 514	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )
Theorem	simp-6l 515	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ph )
Theorem	simp-6r 516	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ps )
Theorem	simp-7l 517	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> ph )
Theorem	simp-7r 518	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) -> ps )
Theorem	simp-8l 519	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) -> ph )
Theorem	simp-8r 520	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) -> ps )
Theorem	simp-9l 521	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 522	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 523	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 524	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 525	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 526	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 527	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	a2and 528	Deduction distributing a conjunction as embedded antecedent. (Contributed by AV, 25-Oct-2019.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
|- ( ph -> ( ( ps /\ rh ) -> ( ta -> th ) ) )   &    |- ( ph -> ( ( ps /\ rh ) -> ch ) )   =>    |- ( ph -> ( ( ( ps /\ ch ) -> ta ) -> ( ( ps /\ rh ) -> th ) ) )
Theorem	animpimp2impd 529	Deduction deriving nested implications from conjunctions. (Contributed by AV, 21-Aug-2022.)
|- ( ( ps /\ ph ) -> ( ch -> ( th -> et ) ) )   &    |- ( ( ps /\ ( ph /\ th ) ) -> ( et -> ta ) )   =>    |- ( ph -> ( ( ps -> ch ) -> ( ps -> ( th -> ta ) ) ) )
Theorem	abai 530	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 531	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 532	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 533	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 534	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 535	Swap two conjuncts in antecedent. The label suffix "s" means that an12 531 is combined with syl 14 (or a variant). (Contributed by NM, 13-Mar-1996.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ps /\ ( ph /\ ch ) ) -> th )
Theorem	ancom2s 536	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 537	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ch /\ ( ps /\ ph ) ) -> th )
Theorem	an32s 538	Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ph /\ ch ) /\ ps ) -> th )
Theorem	ancom1s 539	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 540	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ch /\ ps ) /\ ph ) -> th )
Theorem	anass1rs 541	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 542	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 543	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 544	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 545	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 546	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 547	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.)
|- ( ( ( ps /\ ph ) /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabss5 548	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 549	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 550	Absorption of antecedent into conjunction. (Contributed by NM, 14-Aug-2000.)
|- ( ph -> ( ( ps /\ ph ) -> ch ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabsi7 551	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 552	Absorption of antecedent into conjunction. (Contributed by NM, 26-Sep-1999.)
|- ( ps -> ( ( ps /\ ph ) -> ch ) )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	anabss7 553	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 554	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 555	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 556	Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch ) /\ ( ps /\ th ) ) )
Theorem	an42 557	Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch ) /\ ( th /\ ps ) ) )
Theorem	an4s 558	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )
Theorem	an42s 559	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ( ph /\ ch ) /\ ( th /\ ps ) ) -> ta )
Theorem	anandi 560	Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
|- ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
Theorem	anandir 561	Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ph /\ ch ) /\ ( ps /\ ch ) ) )
Theorem	anandis 562	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
|- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) -> ta )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> ta )
Theorem	anandirs 563	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
|- ( ( ( ph /\ ch ) /\ ( ps /\ ch ) ) -> ta )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> ta )
Theorem	syl2an2 564	syl2an 285 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 565	syl2anr 286 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 566	Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ ch ) -> ps )   =>    |- ( ph -> ( ps <-> ch ) )
Theorem	pm3.45 567	Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ps ) -> ( ( ph /\ ch ) -> ( ps /\ ch ) ) )
Theorem	im2anan9 568	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 569	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 570	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 571	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 572	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 573	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 574	Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) <-> ( ph -> ( ps /\ ch ) ) )
Theorem	pm4.38 575	Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph <-> ch ) /\ ( ps <-> th ) ) -> ( ( ph /\ ps ) <-> ( ch /\ th ) ) )
Theorem	bi2anan9 576	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 577	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 578	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 579	Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph /\ ( ps -> ch ) ) <-> ( ph /\ ( ( ph /\ ps ) -> ch ) ) )
Theorem	pm5.36 580	Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph /\ ( ph <-> ps ) ) <-> ( ps /\ ( ph <-> ps ) ) )
Theorem	bianabs 581	Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.)
|- ( ph -> ( ps <-> ( ph /\ ch ) ) )   =>    |- ( ph -> ( ps <-> ch ) )
Theorem	biadani 582	An implication implies to the equivalence of some implied equivalence and some other equivalence involving a conjunction. (Contributed by BJ, 4-Mar-2023.)
|- ( ph -> ps )   =>    |- ( ( ps -> ( ph <-> ch ) ) <-> ( ph <-> ( ps /\ ch ) ) )
Theorem	biadanii 583	Inference associated with biadani 582. Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) (Proof shortened by BJ, 4-Mar-2023.)
|- ( ph -> ps )   &    |- ( ps -> ( ph <-> ch ) )   =>    |- ( ph <-> ( ps /\ ch ) )
1.2.5  Logical negation (intuitionistic)
Axiom	ax-in1 584	'Not' introduction. One of the axioms of propositional logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- ( ( ph -> -. ph ) -> -. ph )
Axiom	ax-in2 585	'Not' elimination. One of the axioms of propositional logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- ( -. ph -> ( ph -> ps ) )
Theorem	pm2.01 586	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 794 which only holds for some propositions. (Contributed by Mario Carneiro, 12-May-2015.)
|- ( ( ph -> -. ph ) -> -. ph )
Theorem	pm2.21 587	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 588	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 589	A contradiction implies anything. Deduction from pm2.21 587. (Contributed by NM, 10-Feb-1996.)
|- ( ph -> -. ps )   =>    |- ( ph -> ( ps -> ch ) )
Theorem	pm2.21dd 590	A contradiction implies anything. Deduction from pm2.21 587. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ph -> ps )   &    |- ( ph -> -. ps )   =>    |- ( ph -> ch )
Theorem	pm2.24 591	Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
|- ( ph -> ( -. ph -> ps ) )
Theorem	pm2.24d 592	Deduction version of pm2.24 591. (Contributed by NM, 30-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ( ph -> ps )   =>    |- ( ph -> ( -. ps -> ch ) )
Theorem	pm2.24i 593	Inference version of pm2.24 591. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ph   =>    |- ( -. ph -> ps )
Theorem	con2d 594	A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised by NM, 12-Feb-2013.)
|- ( ph -> ( ps -> -. ch ) )   =>    |- ( ph -> ( ch -> -. ps ) )
Theorem	mt2d 595	Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
|- ( ph -> ch )   &    |- ( ph -> ( ps -> -. ch ) )   =>    |- ( ph -> -. ps )
Theorem	nsyl3 596	A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) (Revised by NM, 13-Jun-2013.)
|- ( ph -> -. ps )   &    |- ( ch -> ps )   =>    |- ( ch -> -. ph )
Theorem	con2i 597	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 598	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 599	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 795). (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
|- ( ph -> -. -. ph )
Theorem	notnotd 600	Deduction associated with notnot 599 and notnoti 614. (Contributed by Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf Lammen, 27-Mar-2021.)
|- ( ph -> ps )   =>    |- ( ph -> -. -. ps )