P. 6 of Theorem List - Intuitionistic Logic Explorer

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 501-600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	anabss3 501	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 502	Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
|- (((ph /\ ps) /\ (ch /\ th)) <-> ((ph /\ ch) /\ (ps /\ th)))
Theorem	an42 503	Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
|- (((ph /\ ps) /\ (ch /\ th)) <-> ((ph /\ ch) /\ (th /\ ps)))
Theorem	an4s 504	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
|- (((ph /\ ps) /\ (ch /\ th)) -> ta)   =>   |- (((ph /\ ch) /\ (ps /\ th)) -> ta)
Theorem	an42s 505	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
|- (((ph /\ ps) /\ (ch /\ th)) -> ta)   =>   |- (((ph /\ ch) /\ (th /\ ps)) -> ta)
Theorem	anandi 506	Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
|- ((ph /\ (ps /\ ch)) <-> ((ph /\ ps) /\ (ph /\ ch)))
Theorem	anandir 507	Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.)
|- (((ph /\ ps) /\ ch) <-> ((ph /\ ch) /\ (ps /\ ch)))
Theorem	anandis 508	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
|- (((ph /\ ps) /\ (ph /\ ch)) -> ta)   =>   |- ((ph /\ (ps /\ ch)) -> ta)
Theorem	anandirs 509	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
|- (((ph /\ ch) /\ (ps /\ ch)) -> ta)   =>   |- (((ph /\ ps) /\ ch) -> ta)
Theorem	impbida 510	Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ ch) -> ps)   =>   |- (ph -> (ps <-> ch))
Theorem	pm3.45 511	Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- ((ph -> ps) -> ((ph /\ ch) -> (ps /\ ch)))
Theorem	im2anan9 512	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 513	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 514	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 515	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 516	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 517	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	pm3.43OLD 518	Obsolete proof of pm3.43 516 as of 27-Nov-2013 (Contributed by NM, 3-Jan-2005.)
|- (((ph -> ps) /\ (ph -> ch)) -> (ph -> (ps /\ ch)))
Theorem	pm4.76 519	Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
|- (((ph -> ps) /\ (ph -> ch)) <-> (ph -> (ps /\ ch)))
Theorem	pm4.38 520	Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
|- (((ph <-> ch) /\ (ps <-> th)) -> ((ph /\ ps) <-> (ch /\ th)))
Theorem	bi2anan9 521	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 522	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 523	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 524	Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ((ph /\ (ps -> ch)) <-> (ph /\ ((ph /\ ps) -> ch)))
Theorem	pm5.36 525	Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ((ph /\ (ph <-> ps)) <-> (ps /\ (ph <-> ps)))
Theorem	bianabs 526	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 527	'Not' introduction. Axiom 4 of 10 for intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- ((ph -> -. ph) -> -. ph)
Axiom	ax-in2 528	'Not' elimination. Axiom 5 of 10 for intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- (-. ph -> (ph -> ps))
Theorem	pm2.01 529	Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100. This is valid intuitionistically (in the terminology of [Bauer] p. 482 it is a proof of negation not a proof by contradiction); compare with pm2.18 1955 which is not. (Contributed by Mario Carneiro, 12-May-2015.)
|- ((ph -> -. ph) -> -. ph)
Theorem	pm2.21 530	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 531	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 532	A contradiction implies anything. Deduction from pm2.21 530. (Contributed by NM, 10-Feb-1996.)
|- (ph -> -. ps)   =>   |- (ph -> (ps -> ch))
Theorem	pm2.24 533	Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
|- (ph -> (-. ph -> ps))
Theorem	pm2.24d 534	Deduction version of pm2.24 533. (Contributed by NM, 30-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- (ph -> ps)   =>   |- (ph -> (-. ps -> ch))
Theorem	pm2.24i 535	Inference version of pm2.24 533. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ph   =>   |- (-. ph -> ps)
Theorem	con2d 536	A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised by NM, 12-Feb-2013.)
|- (ph -> (ps -> -. ch))   =>   |- (ph -> (ch -> -. ps))
Theorem	mt2d 537	Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
|- (ph -> ch)   &   |- (ph -> (ps -> -. ch))   =>   |- (ph -> -. ps)
Theorem	nsyl3 538	A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) (Revised by NM, 13-Jun-2013.)
|- (ph -> -. ps)   &   |- (ch -> ps)   =>   |- (ch -> -. ph)
Theorem	con2i 539	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 540	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	notnot1 541	Adding double negation. Theorem *2.12 of [WhiteheadRussell] p. 101. This one holds intuitionistically, but its converse, notnot2 1962, does not. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
|- (ph -> -. -. ph)
Theorem	con3d 542	A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.)
|- (ph -> (ps -> ch))   =>   |- (ph -> (-. ch -> -. ps))
Theorem	con3i 543	A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)
|- (ph -> ps)   =>   |- (-. ps -> -. ph)
Theorem	con3rr3 544	Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.)
|- (ph -> (ps -> ch))   =>   |- (-. ch -> (ph -> -. ps))
Theorem	con3and 545	Variant of con3d 542 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph -> (ps -> ch))   =>   |- ((ph /\ -. ch) -> -. ps)
Theorem	pm3.2im 546	In classical logic, this is just a restatement of pm3.2 124. 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 547	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 548	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 549	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 550	Theorem used to justify definition of intuitionistic biconditional df-bi 108. (Contributed by NM, 24-Nov-2017.)
|- ((((ph -> ps) /\ (ps -> ph)) -> ((ph -> ps) /\ (ps -> ph))) /\ (((ph -> ps) /\ (ps -> ph)) -> ((ph -> ps) /\ (ps -> ph))))
Theorem	con3 551	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 552	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 553	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 554	Infer double negation. (Contributed by NM, 27-Feb-2008.)
|- ph   =>   |- -. -. ph
Theorem	pm2.21i 555	A contradiction implies anything. Inference from pm2.21 530. (Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- -. ph   =>   |- (ph -> ps)
Theorem	pm2.24ii 556	A contradiction implies anything. Inference from pm2.24 533. (Contributed by NM, 27-Feb-2008.)
|- ph   &   |- -. ph   =>   |- ps
Theorem	nsyld 557	A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.)
|- (ph -> (ps -> -. ch))   &   |- (ph -> (ta -> ch))   =>   |- (ph -> (ps -> -. ta))
Theorem	nsyli 558	A negated syllogism inference. (Contributed by NM, 3-May-1994.)
|- (ph -> (ps -> ch))   &   |- (th -> -. ch)   =>   |- (ph -> (th -> -. ps))
Theorem	mth8 559	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 560	Inference joining the consequents of two premises. (Contributed by NM, 5-Aug-1993.)
|- (ph -> ps)   &   |- (ph -> ch)   =>   |- (ph -> -. (ps -> -. ch))
Theorem	pm2.51 561	Theorem *2.51 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
|- (-. (ph -> ps) -> (ph -> -. ps))
Theorem	pm2.52 562	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 563	Exportation theorem expressed with primitive connectives. (Contributed by NM, 5-Aug-1993.)
|- ((-. (ph -> -. ps) -> ch) -> (ph -> (ps -> ch)))
Theorem	jarl 564	Elimination of a nested antecedent. Although it is a kind of reversal of inference ja 1960 it holds intuitionistically, while ja 1960 does not. (Contributed by Wolf Lammen, 10-May-2013.)
|- (((ph -> ps) -> ch) -> (-. ph -> ch))
Theorem	pm2.65 565	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 [Bauer] p. 482). By contrast, proofs which assume -. ph, derive a contradiction, and conclude ph, such as condandc 746, 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 566	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 567	Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.)
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ ps) -> -. ch)   =>   |- (ph -> -. ps)
Theorem	mto 568	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 569	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 570	Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
|- -. ch   &   |- (ph -> (ps -> ch))   =>   |- (ph -> -. ps)
Theorem	mtand 571	A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
|- (ph -> -. ch)   &   |- ((ph /\ ps) -> ch)   =>   |- (ph -> -. ps)
Theorem	notbid 572	Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> (-. ps <-> -. ch))
Theorem	con2b 573	Contraposition. Bidirectional version of con2 552. (Contributed by NM, 5-Aug-1993.)
|- ((ph -> -. ps) <-> (ps -> -. ph))
Theorem	notbii 574	Negate both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- (ph <-> ps)   =>   |- (-. ph <-> -. ps)
Theorem	mtbi 575	An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
|- -. ph   &   |- (ph <-> ps)   =>   |- -. ps
Theorem	mtbir 576	An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.)
|- -. ps   &   |- (ph <-> ps)   =>   |- -. ph
Theorem	mtbid 577	A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)
|- (ph -> -. ps)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ch)
Theorem	mtbird 578	A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.)
|- (ph -> -. ch)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ps)
Theorem	mtbii 579	An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.)
|- -. ps   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ch)
Theorem	mtbiri 580	An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.)
|- -. ch   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ps)
Theorem	sylnib 581	A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)
|- (ph -> -. ps)   &   |- (ps <-> ch)   =>   |- (ph -> -. ch)
Theorem	sylnibr 582	A mixed syllogism inference from an implication and a biconditional. Useful for substituting an consequent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)
|- (ph -> -. ps)   &   |- (ch <-> ps)   =>   |- (ph -> -. ch)
Theorem	sylnbi 583	A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)
|- (ph <-> ps)   &   |- (-. ps -> ch)   =>   |- (-. ph -> ch)
Theorem	sylnbir 584	A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.)
|- (ps <-> ph)   &   |- (-. ps -> ch)   =>   |- (-. ph -> ch)
Theorem	xchnxbi 585	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
|- (-. ph <-> ps)   &   |- (ph <-> ch)   =>   |- (-. ch <-> ps)
Theorem	xchnxbir 586	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
|- (-. ph <-> ps)   &   |- (ch <-> ph)   =>   |- (-. ch <-> ps)
Theorem	xchbinx 587	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
|- (ph <-> -. ps)   &   |- (ps <-> ch)   =>   |- (ph <-> -. ch)
Theorem	xchbinxr 588	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
|- (ph <-> -. ps)   &   |- (ch <-> ps)   =>   |- (ph <-> -. ch)
Theorem	mt2bi 589	A false consequent falsifies an antecedent. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)
|- ph   =>   |- (-. ps <-> (ps -> -. ph))
Theorem	mtt 590	Modus-tollens-like theorem. (Contributed by NM, 7-Apr-2001.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- (-. ph -> (-. ps <-> (ps -> ph)))
Theorem	pm5.21 591	Two propositions are equivalent if they are both false. Theorem *5.21 of [WhiteheadRussell] p. 124. (Contributed by NM, 21-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- ((-. ph /\ -. ps) -> (ph <-> ps))
Theorem	pm5.21im 592	Two propositions are equivalent if they are both false. Closed form of 2false 597. Equivalent to a bi2 119-like version of the xor-connective. (Contributed by Wolf Lammen, 13-May-2013.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- (-. ph -> (-. ps -> (ph <-> ps)))
Theorem	nbn2 593	The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by Juha Arpiainen, 19-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- (-. ph -> (-. ps <-> (ph <-> ps)))
Theorem	bibif 594	Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007.) (Proof shortened by Wolf Lammen, 28-Jan-2013.)
|- (-. ps -> ((ph <-> ps) <-> -. ph))
Theorem	nbn 595	The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
|- -. ph   =>   |- (-. ps <-> (ps <-> ph))
Theorem	nbn3 596	Transfer falsehood via equivalence. (Contributed by NM, 11-Sep-2006.)
|- ph   =>   |- (-. ps <-> (ps <-> -. ph))
Theorem	2false 597	Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- -. ph   &   |- -. ps   =>   |- (ph <-> ps)
Theorem	2falsed 598	Two falsehoods are equivalent (deduction rule). (Contributed by NM, 11-Oct-2013.)
|- (ph -> -. ps)   &   |- (ph -> -. ch)   =>   |- (ph -> (ps <-> ch))
Theorem	pm5.21ni 599	Two propositions implying a false one are equivalent. (Contributed by NM, 16-Feb-1996.) (Proof shortened by Wolf Lammen, 19-May-2013.)
|- (ph -> ps)   &   |- (ch -> ps)   =>   |- (-. ps -> (ph <-> ch))
Theorem	pm5.21nii 600	Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- (ph -> ps)   &   |- (ch -> ps)   &   |- (ps -> (ph <-> ch))   =>   |- (ph <-> ch)