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. (The proof was shortened by Wolf Lammen, 1-Jan-2013.)
|- (((ph /\ ps) /\ ps) -> ch)   =>   |- ((ph /\ ps) -> ch)
Theorem	an4 502	Rearrangement of 4 conjuncts.
|- (((ph /\ ps) /\ (ch /\ th)) <-> ((ph /\ ch) /\ (ps /\ th)))
Theorem	an42 503	Rearrangement of 4 conjuncts.
|- (((ph /\ ps) /\ (ch /\ th)) <-> ((ph /\ ch) /\ (th /\ ps)))
Theorem	an4s 504	Inference rearranging 4 conjuncts in antecedent.
|- (((ph /\ ps) /\ (ch /\ th)) -> ta)   =>   |- (((ph /\ ch) /\ (ps /\ th)) -> ta)
Theorem	an42s 505	Inference rearranging 4 conjuncts in antecedent.
|- (((ph /\ ps) /\ (ch /\ th)) -> ta)   =>   |- (((ph /\ ch) /\ (th /\ ps)) -> ta)
Theorem	anandi 506	Distribution of conjunction over conjunction.
|- ((ph /\ (ps /\ ch)) <-> ((ph /\ ps) /\ (ph /\ ch)))
Theorem	anandir 507	Distribution of conjunction over conjunction.
|- (((ph /\ ps) /\ ch) <-> ((ph /\ ch) /\ (ps /\ ch)))
Theorem	anandis 508	Inference that undistributes conjunction in the antecedent.
|- (((ph /\ ps) /\ (ph /\ ch)) -> ta)   =>   |- ((ph /\ (ps /\ ch)) -> ta)
Theorem	anandirs 509	Inference that undistributes conjunction in the antecedent.
|- (((ph /\ ch) /\ (ps /\ ch)) -> ta)   =>   |- (((ph /\ ps) /\ ch) -> ta)
Theorem	impbida 510	Deduce an equivalence from two implications.
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ ch) -> ps)   =>   |- (ph -> (ps <-> ch))
Theorem	pm3.45 511	Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113.
|- ((ph -> ps) -> ((ph /\ ch) -> (ps /\ ch)))
Theorem	im2anan9 512	Deduction joining nested implications to form implication of conjunctions.
|- (ph -> (ps -> ch))   &   |- (th -> (ta -> et))   =>   |- ((ph /\ th) -> ((ps /\ ta) -> (ch /\ et)))
Theorem	im2anan9r 513	Deduction joining nested implications to form implication of conjunctions.
|- (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.
|- ((ph /\ ps) -> (ph <-> ps))
Theorem	pm3.43 516	Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113.
|- (((ph -> ps) /\ (ph -> ch)) -> (ph -> (ps /\ ch)))
Theorem	jcab 517	Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121. (The proof was 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
|- (((ph -> ps) /\ (ph -> ch)) -> (ph -> (ps /\ ch)))
Theorem	pm4.76 519	Theorem *4.76 of [WhiteheadRussell] p. 121.
|- (((ph -> ps) /\ (ph -> ch)) <-> (ph -> (ps /\ ch)))
Theorem	pm4.38 520	Theorem *4.38 of [WhiteheadRussell] p. 118.
|- (((ph <-> ch) /\ (ps <-> th)) -> ((ph /\ ps) <-> (ch /\ th)))
Theorem	bi2anan9 521	Deduction joining two equivalences to form equivalence of conjunctions.
|- (ph -> (ps <-> ch))   &   |- (th -> (ta <-> et))   =>   |- ((ph /\ th) -> ((ps /\ ta) <-> (ch /\ et)))
Theorem	bi2anan9r 522	Deduction joining two equivalences to form equivalence of conjunctions.
|- (ph -> (ps <-> ch))   &   |- (th -> (ta <-> et))   =>   |- ((th /\ ph) -> ((ps /\ ta) <-> (ch /\ et)))
Theorem	bi2bian9 523	Deduction joining two biconditionals with different antecedents.
|- (ph -> (ps <-> ch))   &   |- (th -> (ta <-> et))   =>   |- ((ph /\ th) -> ((ps <-> ta) <-> (ch <-> et)))
Theorem	pm5.33 524	Theorem *5.33 of [WhiteheadRussell] p. 125.
|- ((ph /\ (ps -> ch)) <-> (ph /\ ((ph /\ ps) -> ch)))
Theorem	pm5.36 525	Theorem *5.36 of [WhiteheadRussell] p. 125.
|- ((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.
|- ((ph -> -. ph) -> -. ph)
Axiom	ax-in2 528	'Not' elimination. Axiom 5 of 10 for intuitionistic logic.
|- (-. ph -> (ph -> ps))
Theorem	pm2.01 529	Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100. (The proof was shortened by O'Cat, 21-Nov-2008.) (The proof was shortened by Wolf Lammen, 31-Oct-2012.)
|- ((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. (The proof was shortened by Wolf Lammen, 14-Sep-2012.)
|- (-. ph -> (ph -> ps))
Theorem	pm2.01d 531	Deduction based on reductio ad absurdum. (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.
|- (ph -> -. ps)   =>   |- (ph -> (ps -> ch))
Theorem	pm2.24 533	Theorem *2.24 of [WhiteheadRussell] p. 104.
|- (ph -> (-. ph -> ps))
Theorem	pm2.24d 534	Deduction version of pm2.24 533. (Revised by Mario Carneiro, 31-Jan-2015.)
|- (ph -> ps)   =>   |- (ph -> (-. ps -> ch))
Theorem	pm2.24i 535	Inference version of pm2.24 533. (Revised by Mario Carneiro, 31-Jan-2015.)
|- ph   =>   |- (-. ph -> ps)
Theorem	con2d 536	A contraposition deduction.
|- (ph -> (ps -> -. ch))   =>   |- (ph -> (ch -> -. ps))
Theorem	mt2d 537	Modus tollens deduction.
|- (ph -> ch)   &   |- (ph -> (ps -> -. ch))   =>   |- (ph -> -. ps)
Theorem	nsyl3 538	A negated syllogism inference.
|- (ph -> -. ps)   &   |- (ch -> ps)   =>   |- (ch -> -. ph)
Theorem	con2i 539	A contraposition inference. (The proof was shortened by O'Cat, 28-Nov-2008.) (The proof was shortened by Wolf Lammen, 13-Jun-2013.)
|- (ph -> -. ps)   =>   |- (ps -> -. ph)
Theorem	nsyl 540	A negated syllogism inference. (The proof was shortened by Wolf Lammen, 2-Mar-2013.)
|- (ph -> -. ps)   &   |- (ch -> ps)   =>   |- (ph -> -. ch)
Theorem	notnot1 541	Converse of double negation. Theorem *2.12 of [WhiteheadRussell] p. 101. (The proof was shortened by Wolf Lammen, 2-Mar-2013.)
|- (ph -> -. -. ph)
Theorem	con3d 542	A contraposition deduction.
|- (ph -> (ps -> ch))   =>   |- (ph -> (-. ch -> -. ps))
Theorem	con3i 543	A contraposition inference. (The proof was 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	pm3.2im 545	Theorem *3.2 of [WhiteheadRussell] p. 111, expressed with primitive connectives. (The proof was shortened by Josh Purinton, 29-Dec-2000.)
|- (ph -> (ps -> -. (ph -> -. ps)))
Theorem	expi 546	An exportation inference. (The proof was shortened by O'Cat, 28-Nov-2008.)
|- (-. (ph -> -. ps) -> ch)   =>   |- (ph -> (ps -> ch))
Theorem	pm2.65i 547	Inference rule for proof by contradiction. (The proof was shortened by Wolf Lammen, 11-Sep-2013.)
|- (ph -> ps)   &   |- (ph -> -. ps)   =>   |- -. ph
Theorem	mt2 548	A rule similar to modus tollens. (The proof was shortened by Wolf Lammen, 10-Sep-2013.)
|- ps   &   |- (ph -> -. ps)   =>   |- -. ph
Theorem	bijust 549	Theorem used to justify definition of biconditional df-bi 109. (The proof was shortened by Josh Purinton, 29-Dec-2000.)
|- -. ((-. ((ph -> ps) -> -. (ps -> ph)) -> -. ((ph -> ps) -> -. (ps -> ph))) -> -. (-. ((ph -> ps) -> -. (ps -> ph)) -> -. ((ph -> ps) -> -. (ps -> ph))))
Theorem	con3 550	Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. (The proof was shortened by Wolf Lammen, 13-Feb-2013.)
|- ((ph -> ps) -> (-. ps -> -. ph))
Theorem	con2 551	Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (The proof was shortened by Wolf Lammen, 12-Feb-2013.)
|- ((ph -> -. ps) -> (ps -> -. ph))
Theorem	mt2i 552	Modus tollens inference. (The proof was shortened by Wolf Lammen, 15-Sep-2012.)
|- ch   &   |- (ph -> (ps -> -. ch))   =>   |- (ph -> -. ps)
Theorem	notnoti 553	Infer double negation.
|- ph   =>   |- -. -. ph
Theorem	pm2.21i 554	A contradiction implies anything. Inference from pm2.21 530. (Revised by Mario Carneiro, 31-Jan-2015.)
|- -. ph   =>   |- (ph -> ps)
Theorem	pm2.24ii 555	A contradiction implies anything. Inference from pm2.24 533.
|- ph   &   |- -. ph   =>   |- ps
Theorem	nsyld 556	A negated syllogism deduction.
|- (ph -> (ps -> -. ch))   &   |- (ph -> (ta -> ch))   =>   |- (ph -> (ps -> -. ta))
Theorem	nsyli 557	A negated syllogism inference.
|- (ph -> (ps -> ch))   &   |- (th -> -. ch)   =>   |- (ph -> (th -> -. ps))
Theorem	mth8 558	Theorem 8 of [Margaris] p. 60. (The proof was shortened by Josh Purinton, 29-Dec-2000.)
|- (ph -> (-. ps -> -. (ph -> ps)))
Theorem	jc 559	Inference joining the consequents of two premises.
|- (ph -> ps)   &   |- (ph -> ch)   =>   |- (ph -> -. (ps -> -. ch))
Theorem	pm2.51 560	Theorem *2.51 of [WhiteheadRussell] p. 107.
|- (-. (ph -> ps) -> (ph -> -. ps))
Theorem	pm2.52 561	Theorem *2.52 of [WhiteheadRussell] p. 107. (Revised by Mario Carneiro, 31-Jan-2015.)
|- (-. (ph -> ps) -> (-. ph -> -. ps))
Theorem	expt 562	Exportation theorem expressed with primitive connectives.
|- ((-. (ph -> -. ps) -> ch) -> (ph -> (ps -> ch)))
Theorem	jarl 563	Elimination of a nested antecedent as a kind of reversal of inference ja 738. (Contributed by Wolf Lammen, 10-May-2013.)
|- (((ph -> ps) -> ch) -> (-. ph -> ch))
Theorem	pm2.65 564	Theorem *2.65 of [WhiteheadRussell] p. 107. Proof by contradiction. (The proof was shortened by Wolf Lammen, 8-Mar-2013.)
|- ((ph -> ps) -> ((ph -> -. ps) -> -. ph))
Theorem	pm2.65d 565	Deduction rule for proof by contradiction. (The proof was shortened by Wolf Lammen, 26-May-2013.)
|- (ph -> (ps -> ch))   &   |- (ph -> (ps -> -. ch))   =>   |- (ph -> -. ps)
Theorem	pm2.65da 566	Deduction rule for proof by contradiction.
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ ps) -> -. ch)   =>   |- (ph -> -. ps)
Theorem	mto 567	The rule of modus tollens. (The proof was shortened by Wolf Lammen, 11-Sep-2013.)
|- -. ps   &   |- (ph -> ps)   =>   |- -. ph
Theorem	mtod 568	Modus tollens deduction. (The proof was shortened by Wolf Lammen, 11-Sep-2013.)
|- (ph -> -. ch)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> -. ps)
Theorem	mtoi 569	Modus tollens inference. (The proof was shortened by Wolf Lammen, 15-Sep-2012.)
|- -. ch   &   |- (ph -> (ps -> ch))   =>   |- (ph -> -. ps)
Theorem	mtand 570	A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
|- (ph -> -. ch)   &   |- ((ph /\ ps) -> ch)   =>   |- (ph -> -. ps)
Theorem	notbid 571	Deduction negating both sides of a logical equivalence. (Revised by Mario Carneiro, 31-Jan-2015.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> (-. ps <-> -. ch))
Theorem	con2b 572	Contraposition. Bidirectional version of con2 551.
|- ((ph -> -. ps) <-> (ps -> -. ph))
Theorem	notbii 573	Negate both sides of a logical equivalence. (Revised by Mario Carneiro, 31-Jan-2015.)
|- (ph <-> ps)   =>   |- (-. ph <-> -. ps)
Theorem	mtbi 574	An inference from a biconditional, related to modus tollens. (The proof was shortened by Wolf Lammen, 25-Oct-2012.)
|- -. ph   &   |- (ph <-> ps)   =>   |- -. ps
Theorem	mtbir 575	An inference from a biconditional, related to modus tollens. (The proof was shortened by Wolf Lammen, 14-Oct-2012.)
|- -. ps   &   |- (ph <-> ps)   =>   |- -. ph
Theorem	mtbid 576	A deduction from a biconditional, similar to modus tollens.
|- (ph -> -. ps)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ch)
Theorem	mtbird 577	A deduction from a biconditional, similar to modus tollens.
|- (ph -> -. ch)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ps)
Theorem	mtbii 578	An inference from a biconditional, similar to modus tollens.
|- -. ps   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ch)
Theorem	mtbiri 579	An inference from a biconditional, similar to modus tollens.
|- -. ch   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ps)
Theorem	sylnib 580	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 581	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 582	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 583	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 584	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
|- (-. ph <-> ps)   &   |- (ph <-> ch)   =>   |- (-. ch <-> ps)
Theorem	xchnxbir 585	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
|- (-. ph <-> ps)   &   |- (ch <-> ph)   =>   |- (-. ch <-> ps)
Theorem	xchbinx 586	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
|- (ph <-> -. ps)   &   |- (ps <-> ch)   =>   |- (ph <-> -. ch)
Theorem	xchbinxr 587	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
|- (ph <-> -. ps)   &   |- (ch <-> ps)   =>   |- (ph <-> -. ch)
Theorem	mt2bi 588	A false consequent falsifies an antecedent. (The proof was shortened by Wolf Lammen, 12-Nov-2012.)
|- ph   =>   |- (-. ps <-> (ps -> -. ph))
Theorem	mtt 589	Modus-tollens-like theorem. (Revised by Mario Carneiro, 31-Jan-2015.)
|- (-. ph -> (-. ps <-> (ps -> ph)))
Theorem	pm5.21 590	Two propositions are equivalent if they are both false. Theorem *5.21 of [WhiteheadRussell] p. 124. (Revised by Mario Carneiro, 31-Jan-2015.)
|- ((-. ph /\ -. ps) -> (ph <-> ps))
Theorem	pm5.21im 591	Two propositions are equivalent if they are both false. Closed form of 2false 596. Equivalent to a bi2 120-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 592	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 593	Transfer negation via an equivalence. (The proof was shortened by Wolf Lammen, 28-Jan-2013.)
|- (-. ps -> ((ph <-> ps) <-> -. ph))
Theorem	nbn 594	The negation of a wff is equivalent to the wff's equivalence to falsehood. (The proof was shortened by Wolf Lammen, 3-Oct-2013.)
|- -. ph   =>   |- (-. ps <-> (ps <-> ph))
Theorem	nbn3 595	Transfer falsehood via equivalence.
|- ph   =>   |- (-. ps <-> (ps <-> -. ph))
Theorem	2false 596	Two falsehoods are equivalent. (Revised by Mario Carneiro, 31-Jan-2015.)
|- -. ph   &   |- -. ps   =>   |- (ph <-> ps)
Theorem	2falsed 597	Two falsehoods are equivalent (deduction rule).
|- (ph -> -. ps)   &   |- (ph -> -. ch)   =>   |- (ph -> (ps <-> ch))
Theorem	pm5.21ni 598	Two propositions implying a false one are equivalent. (The proof was shortened by Wolf Lammen, 19-May-2013.)
|- (ph -> ps)   &   |- (ch -> ps)   =>   |- (-. ps -> (ph <-> ch))
Theorem	pm5.21nii 599	Eliminate an antecedent implied by each side of a biconditional. (Revised by Mario Carneiro, 31-Jan-2015.)
|- (ph -> ps)   &   |- (ch -> ps)   &   |- (ps -> (ph <-> ch))   =>   |- (ph <-> ch)
Theorem	pm5.21ndd 600	Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Revised by Mario Carneiro, 31-Jan-2015.)
|- (ph -> (ch -> ps))   &   |- (ph -> (th -> ps))   &   |- (ph -> (ps -> (ch <-> th)))   =>   |- (ph -> (ch <-> th))