Metamath Proof Explorer - mmtheorems6

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 501-600 - Page 6 of 58

Type	Label	Description
Statement
Theorem	pm5.1 501	Two propositions are equivalent if they are both true. Theorem *5.1 of [WhiteheadRussell] p. 123.
|- ((ph /\ ps) -> (ph <-> ps))
Theorem	pm5.21 502	Two propositions are equivalent if they are both false. Theorem *5.21 of [WhiteheadRussell] p. 124.
|- ((-. ph /\ -. ps) -> (ph <-> ps))
Theorem	pm5.21ni 503	Two propositions implying a false one are equivalent.
|- (ph -> ps)   &   |- (ch -> ps)   =>   |- (-. ps -> (ph <-> ch))
Theorem	pm5.21nii 504	Elimination of antecedent implied by each side of biconditional.
|- (ph -> ps)   &   |- (ch -> ps)   &   |- (ps -> (ph <-> ch))   =>   |- (ph <-> ch)
Theorem	elimant 505	Elimination of antecedents in an implication.
|- (((ph -> ps) /\ ((ps -> ch) -> (ph -> th))) -> (ph -> (ch -> th)))
Theorem	baib 506	Move conjunction outside of biconditional.
|- (ph <-> (ps /\ ch))   =>   |- (ps -> (ph <-> ch))
Theorem	baibr 507	Move conjunction outside of biconditional.
|- (ph <-> (ps /\ ch))   =>   |- (ps -> (ch <-> ph))
Theorem	msca 508	Syllogism combined with contraposition.
|- (ph -> (ps -> ch))   &   |- (th -> (ps -> -. ch))   =>   |- (ph -> (ps -> -. th))
Theorem	orcana 509	Disjunction in consequent versus conjunction in antecedent. Similar to Theorem *5.6 of [WhiteheadRussell] p. 125.
|- ((ph -> (ps \/ ch)) <-> ((ph /\ -. ps) -> ch))
Theorem	orbidi 510	Disjunction distributes over the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseer.lcs.mit.edu/lifschitz98calculational.html.
|- ((ph \/ (ps <-> ch)) <-> ((ph \/ ps) <-> (ph \/ ch)))
Theorem	biass 511	Associative law for the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseer.lcs.mit.edu/lifschitz98calculational.html. Noted by Jan Lukasiewicz c. 1923.
|- (((ph <-> ps) <-> ch) <-> (ph <-> (ps <-> ch)))
Theorem	biluk 512	Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall, ed., Polish Logic 1920-1939 (Oxford, 1967), p. 96.
|- ((ph <-> ps) <-> ((ch <-> ps) <-> (ph <-> ch)))
Theorem	bigolden 513	Dijkstra-Scholten's Golden Rule for calculational proofs.
|- (((ph /\ ps) <-> ph) <-> (ps <-> (ph \/ ps)))
Theorem	nan 514	Theorem to move a conjunct in and out of a negation.
|- ((ph -> -. (ps /\ ch)) <-> ((ph /\ ps) -> -. ch))
Theorem	orcanai 515	Change disjunction in consequent to conjunction in antecedent.
|- (ph -> (ps \/ ch))   =>   |- ((ph /\ -. ps) -> ch)
Theorem	intnan 516	Introduction of conjunct inside of a contradiction.
|- -. ph   =>   |- -. (ps /\ ph)
Theorem	intnanr 517	Introduction of conjunct inside of a contradiction.
|- -. ph   =>   |- -. (ph /\ ps)
Theorem	mpan 518	An inference based on modus ponens.
|- ph   &   |- ((ph /\ ps) -> ch)   =>   |- (ps -> ch)
Theorem	mpan2 519	An inference based on modus ponens.
|- ps   &   |- ((ph /\ ps) -> ch)   =>   |- (ph -> ch)
Theorem	mp2an 520	An inference based on modus ponens.
|- ph   &   |- ps   &   |- ((ph /\ ps) -> ch)   =>   |- ch
Theorem	mpani 521	An inference based on modus ponens.
|- ps   &   |- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> (ch -> th))
Theorem	mpan2i 522	An inference based on modus ponens.
|- ch   &   |- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> (ps -> th))
Theorem	mp2ani 523	An inference based on modus ponens.
|- ps   &   |- ch   &   |- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> th)
Theorem	mpand 524	A deduction based on modus ponens.
|- (ph -> ps)   &   |- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> (ch -> th))
Theorem	mpan2d 525	A deduction based on modus ponens.
|- (ph -> ch)   &   |- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> (ps -> th))
Theorem	mp2and 526	A deduction based on modus ponens.
|- (ph -> ps)   &   |- (ph -> ch)   &   |- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> th)
Theorem	mpdan 527	An inference based on modus ponens.
|- (ph -> ps)   &   |- ((ph /\ ps) -> ch)   =>   |- (ph -> ch)
Theorem	mpancom 528	An inference based on modus ponens with commutation of antecedents.
|- (ps -> ph)   &   |- ((ph /\ ps) -> ch)   =>   |- (ps -> ch)
Theorem	mpan11 529	An inference based on modus ponens.
|- ph   &   |- (((ph /\ ps) /\ ch) -> th)   =>   |- ((ps /\ ch) -> th)
Theorem	mpan12 530	An inference based on modus ponens.
|- ps   &   |- (((ph /\ ps) /\ ch) -> th)   =>   |- ((ph /\ ch) -> th)
Theorem	mpan21 531	An inference based on modus ponens.
|- ps   &   |- ((ph /\ (ps /\ ch)) -> th)   =>   |- ((ph /\ ch) -> th)
Theorem	mpan22 532	An inference based on modus ponens.
|- ch   &   |- ((ph /\ (ps /\ ch)) -> th)   =>   |- ((ph /\ ps) -> th)
Theorem	mpan121 533	An inference based on modus ponens.
|- ps   &   |- (((ph /\ (ps /\ ch)) /\ th) -> ta )   =>   |- (((ph /\ ch) /\ th) -> ta )
Theorem	mtt 534	Modus-tollens-like theorem.
|- (-. ph -> (-. ps <-> (ps -> ph)))
Theorem	mt2bi 535	A false consequent falsifies an antecedent.
|- ph   =>   |- (-. ps <-> (ps -> -. ph))
Theorem	mtbid 536	A deduction from a biconditional, similar to modus tollens.
|- (ph -> -. ps)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ch)
Theorem	mtbird 537	A deduction from a biconditional, similar to modus tollens.
|- (ph -> -. ch)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ps)
Theorem	mtbii 538	An inference from a biconditional, similar to modus tollens.
|- -. ps   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ch)
Theorem	mtbiri 539	An inference from a biconditional, similar to modus tollens.
|- -. ch   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> -. ps)
Theorem	2th 540	Two truths are equivalent.
|- ph   &   |- ps   =>   |- (ph <-> ps)
Theorem	tbt 541	A wff is equivalent to its equivalence with truth.
|- ph   =>   |- (ps <-> (ps <-> ph))
Theorem	nbn 542	The negation of a wff is equivalent to the wff's equivalence to falsehood.
|- -. ph   =>   |- (-. ps <-> (ps <-> ph))
Theorem	biantru 543	A wff is equivalent to its conjunction with truth.
|- ph   =>   |- (ps <-> (ps /\ ph))
Theorem	biantrur 544	A wff is equivalent to its conjunction with truth.
|- ph   =>   |- (ps <-> (ph /\ ps))
Theorem	biantrud 545	A wff is equivalent to its conjunction with truth.
|- (ph -> ps)   =>   |- (ph -> (ch <-> (ch /\ ps)))
Theorem	biantrurd 546	A wff is equivalent to its conjunction with truth.
|- (ph -> ps)   =>   |- (ph -> (ch <-> (ps /\ ch)))
Theorem	mpbiran 547	Detach truth from conjunction in biconditional.
|- (ph <-> (ps /\ ch))   &   |- ps   =>   |- (ph <-> ch)
Theorem	mpbiranr 548	Detach truth from conjunction in biconditional.
|- (ph <-> (ps /\ ch))   &   |- ch   =>   |- (ph <-> ps)
Theorem	biimt 549	A wff is equivalent to itself with true antecedent.
|- (ph -> (ps <-> (ph -> ps)))
Theorem	biort 550	A wff is disjoined with truth is true.
|- (ph -> (ph <-> (ph \/ ps)))
Theorem	biorf 551	A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of [WhiteheadRussell] p. 121.
|- (-. ph -> (ps <-> (ph \/ ps)))
Theorem	biorfi 552	A wff is equivalent to its disjunction with falsehood.
|- -. ph   =>   |- (ps <-> (ps \/ ph))
Theorem	bianfi 553	A wff conjoined with falsehood is false.
|- -. ph   =>   |- (ph <-> (ps /\ ph))
Theorem	bianfd 554	A wff conjoined with falsehood is false.
|- (ph -> -. ps)   =>   |- (ph -> (ps <-> (ps /\ ch)))
Theorem	pclem6 555	Negation inferred from embedded conjunct.
|- ((ph <-> (ps /\ -. ph)) -> -. ps)
Theorem	biantr 556	A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117.
|- (((ph <-> ps) /\ (ch <-> ps)) -> (ph <-> ch))
Theorem	bimsc1 557	Removal of conjunct from one side of an equivalence.
|- (((ph -> ps) /\ (ch <-> (ps /\ ph))) -> (ch <-> ph))
Theorem	ecase2d 558	Deduction for elimination by cases.
|- (ph -> ps)   &   |- (ph -> -. (ps /\ ch))   &   |- (ph -> -. (ps /\ th))   &   |- (ph -> (ta \/ (ch \/ th)))   =>   |- (ph -> ta )
Theorem	ecase3 559	Inference for elimination by cases.
|- (ph -> ch)   &   |- (ps -> ch)   &   |- (-. (ph \/ ps) -> ch)   =>   |- ch
Theorem	ecase3d 560	Deduction for elimination by cases.
|- (ph -> (ps -> th))   &   |- (ph -> (ch -> th))   &   |- (ph -> (-. (ps \/ ch) -> th))   =>   |- (ph -> th)
Theorem	caselem 561	Lemma for combining cases.
|- (((ph \/ ps) /\ (ch \/ th)) <-> (((ph /\ ch) \/ (ps /\ ch)) \/ ((ph /\ th) \/ (ps /\ th))))
Theorem	ccase 562	Inference for combining cases.
|- ((ph /\ ps) -> ta )   &   |- ((ch /\ ps) -> ta )   &   |- ((ph /\ th) -> ta )   &   |- ((ch /\ th) -> ta )   =>   |- (((ph \/ ch) /\ (ps \/ th)) -> ta )
Theorem	ccased 563	Deduction for combining cases.
|- (ph -> ((ps /\ ch) -> et))   &   |- (ph -> ((th /\ ch) -> et))   &   |- (ph -> ((ps /\ ta ) -> et))   &   |- (ph -> ((th /\ ta ) -> et))   =>   |- (ph -> (((ps \/ th) /\ (ch \/ ta )) -> et))
Theorem	ccase2 564	Inference for combining cases.
|- ((ph /\ ps) -> ta )   &   |- (ch -> ta )   &   |- (th -> ta )   =>   |- (((ph