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.
⊢ ((φ ∧ ψ) → (φ ↔ ψ))
Theorem	pm5.21 502	Two propositions are equivalent if they are both false. Theorem *5.21 of [WhiteheadRussell] p. 124.
⊢ ((¬ φ ∧ ¬ ψ) → (φ ↔ ψ))
Theorem	pm5.21ni 503	Two propositions implying a false one are equivalent.
⊢ (φ → ψ)    &   ⊢ (χ → ψ)    ⇒   ⊢ (¬ ψ → (φ ↔ χ))
Theorem	pm5.21nii 504	Elimination of antecedent implied by each side of biconditional.
⊢ (φ → ψ)    &   ⊢ (χ → ψ)    &   ⊢ (ψ → (φ ↔ χ))    ⇒   ⊢ (φ ↔ χ)
Theorem	elimant 505	Elimination of antecedents in an implication.
⊢ (((φ → ψ) ∧ ((ψ → χ) → (φ → θ))) → (φ → (χ → θ)))
Theorem	baib 506	Move conjunction outside of biconditional.
⊢ (φ ↔ (ψ ∧ χ))    ⇒   ⊢ (ψ → (φ ↔ χ))
Theorem	baibr 507	Move conjunction outside of biconditional.
⊢ (φ ↔ (ψ ∧ χ))    ⇒   ⊢ (ψ → (χ ↔ φ))
Theorem	msca 508	Syllogism combined with contraposition.
⊢ (φ → (ψ → χ))    &   ⊢ (θ → (ψ → ¬ χ))    ⇒   ⊢ (φ → (ψ → ¬ θ))
Theorem	orcana 509	Disjunction in consequent versus conjunction in antecedent. Similar to Theorem *5.6 of [WhiteheadRussell] p. 125.
⊢ ((φ → (ψ ∨ χ)) ↔ ((φ ∧ ¬ ψ) → χ))
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.
⊢ ((φ ∨ (ψ ↔ χ)) ↔ ((φ ∨ ψ) ↔ (φ ∨ χ)))
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.
⊢ (((φ ↔ ψ) ↔ χ) ↔ (φ ↔ (ψ ↔ χ)))
Theorem	biluk 512	Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall, ed., Polish Logic 1920-1939 (Oxford, 1967), p. 96.
⊢ ((φ ↔ ψ) ↔ ((χ ↔ ψ) ↔ (φ ↔ χ)))
Theorem	bigolden 513	Dijkstra-Scholten's Golden Rule for calculational proofs.
⊢ (((φ ∧ ψ) ↔ φ) ↔ (ψ ↔ (φ ∨ ψ)))
Theorem	nan 514	Theorem to move a conjunct in and out of a negation.
⊢ ((φ → ¬ (ψ ∧ χ)) ↔ ((φ ∧ ψ) → ¬ χ))
Theorem	orcanai 515	Change disjunction in consequent to conjunction in antecedent.
⊢ (φ → (ψ ∨ χ))    ⇒   ⊢ ((φ ∧ ¬ ψ) → χ)
Theorem	intnan 516	Introduction of conjunct inside of a contradiction.
⊢ ¬ φ    ⇒   ⊢ ¬ (ψ ∧ φ)
Theorem	intnanr 517	Introduction of conjunct inside of a contradiction.
⊢ ¬ φ    ⇒   ⊢ ¬ (φ ∧ ψ)
Theorem	mpan 518	An inference based on modus ponens.
⊢ φ    &   ⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (ψ → χ)
Theorem	mpan2 519	An inference based on modus ponens.
⊢ ψ    &   ⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (φ → χ)
Theorem	mp2an 520	An inference based on modus ponens.
⊢ φ    &   ⊢ ψ    &   ⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ χ
Theorem	mpani 521	An inference based on modus ponens.
⊢ ψ    &   ⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ (φ → (χ → θ))
Theorem	mpan2i 522	An inference based on modus ponens.
⊢ χ    &   ⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ (φ → (ψ → θ))
Theorem	mp2ani 523	An inference based on modus ponens.
⊢ ψ    &   ⊢ χ    &   ⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ (φ → θ)
Theorem	mpand 524	A deduction based on modus ponens.
⊢ (φ → ψ)    &   ⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ (φ → (χ → θ))
Theorem	mpan2d 525	A deduction based on modus ponens.
⊢ (φ → χ)    &   ⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ (φ → (ψ → θ))
Theorem	mp2and 526	A deduction based on modus ponens.
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ (φ → θ)
Theorem	mpdan 527	An inference based on modus ponens.
⊢ (φ → ψ)    &   ⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (φ → χ)
Theorem	mpancom 528	An inference based on modus ponens with commutation of antecedents.
⊢ (ψ → φ)    &   ⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (ψ → χ)
Theorem	mpan11 529	An inference based on modus ponens.
⊢ φ    &   ⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ ((ψ ∧ χ) → θ)
Theorem	mpan12 530	An inference based on modus ponens.
⊢ ψ    &   ⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ χ) → θ)
Theorem	mpan21 531	An inference based on modus ponens.
⊢ ψ    &   ⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ χ) → θ)
Theorem	mpan22 532	An inference based on modus ponens.
⊢ χ    &   ⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ ψ) → θ)
Theorem	mpan121 533	An inference based on modus ponens.
⊢ ψ    &   ⊢ (((φ ∧ (ψ ∧ χ)) ∧ θ) → τ)    ⇒   ⊢ (((φ ∧ χ) ∧ θ) → τ)
Theorem	mtt 534	Modus-tollens-like theorem.
⊢ (¬ φ → (¬ ψ ↔ (ψ → φ)))
Theorem	mt2bi 535	A false consequent falsifies an antecedent.
⊢ φ    ⇒   ⊢ (¬ ψ ↔ (ψ → ¬ φ))
Theorem	mtbid 536	A deduction from a biconditional, similar to modus tollens.
⊢ (φ → ¬ ψ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ¬ χ)
Theorem	mtbird 537	A deduction from a biconditional, similar to modus tollens.
⊢ (φ → ¬ χ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	mtbii 538	An inference from a biconditional, similar to modus tollens.
⊢ ¬ ψ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ¬ χ)
Theorem	mtbiri 539	An inference from a biconditional, similar to modus tollens.
⊢ ¬ χ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	2th 540	Two truths are equivalent.
⊢ φ    &   ⊢ ψ    ⇒   ⊢ (φ ↔ ψ)
Theorem	tbt 541	A wff is equivalent to its equivalence with truth.
⊢ φ    ⇒   ⊢ (ψ ↔ (ψ ↔ φ))
Theorem	nbn 542	The negation of a wff is equivalent to the wff's equivalence to falsehood.
⊢ ¬ φ    ⇒   ⊢ (¬ ψ ↔ (ψ ↔ φ))
Theorem	biantru 543	A wff is equivalent to its conjunction with truth.
⊢ φ    ⇒   ⊢ (ψ ↔ (ψ ∧ φ))
Theorem	biantrur 544	A wff is equivalent to its conjunction with truth.
⊢ φ    ⇒   ⊢ (ψ ↔ (φ ∧ ψ))
Theorem	biantrud 545	A wff is equivalent to its conjunction with truth.
⊢ (φ → ψ)    ⇒   ⊢ (φ → (χ ↔ (χ ∧ ψ)))
Theorem	biantrurd 546	A wff is equivalent to its conjunction with truth.
⊢ (φ → ψ)    ⇒   ⊢ (φ → (χ ↔ (ψ ∧ χ)))
Theorem	mpbiran 547	Detach truth from conjunction in biconditional.
⊢ (φ ↔ (ψ ∧ χ))    &   ⊢ ψ    ⇒   ⊢ (φ ↔ χ)
Theorem	mpbiranr 548	Detach truth from conjunction in biconditional.
⊢ (φ ↔ (ψ ∧ χ))    &   ⊢ χ    ⇒   ⊢ (φ ↔ ψ)
Theorem	biimt 549	A wff is equivalent to itself with true antecedent.
⊢ (φ → (ψ ↔ (φ → ψ)))
Theorem	biort 550	A wff is disjoined with truth is true.
⊢ (φ → (φ ↔ (φ ∨ ψ)))
Theorem	biorf 551	A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of [WhiteheadRussell] p. 121.
⊢ (¬ φ → (ψ ↔ (φ ∨ ψ)))
Theorem	biorfi 552	A wff is equivalent to its disjunction with falsehood.
⊢ ¬ φ    ⇒   ⊢ (ψ ↔ (ψ ∨ φ))
Theorem	bianfi 553	A wff conjoined with falsehood is false.
⊢ ¬ φ    ⇒   ⊢ (φ ↔ (ψ ∧ φ))
Theorem	bianfd 554	A wff conjoined with falsehood is false.
⊢ (φ → ¬ ψ)    ⇒   ⊢ (φ → (ψ ↔ (ψ ∧ χ)))
Theorem	pclem6 555	Negation inferred from embedded conjunct.
⊢ ((φ ↔ (ψ ∧ ¬ φ)) → ¬ ψ)
Theorem	biantr 556	A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117.
⊢ (((φ ↔ ψ) ∧ (χ ↔ ψ)) → (φ ↔ χ))
Theorem	bimsc1 557	Removal of conjunct from one side of an equivalence.
⊢ (((φ → ψ) ∧ (χ ↔ (ψ ∧ φ))) → (χ ↔ φ))
Theorem	ecase2d 558	Deduction for elimination by cases.
⊢ (φ → ψ)    &   ⊢ (φ → ¬ (ψ ∧ χ))    &   ⊢ (φ → ¬ (ψ ∧ θ))    &   ⊢ (φ → (τ ∨ (χ ∨ θ)))    ⇒   ⊢ (φ → τ)
Theorem	ecase3 559	Inference for elimination by cases.
⊢ (φ → χ)    &   ⊢ (ψ → χ)    &   ⊢ (¬ (φ ∨ ψ) → χ)    ⇒   ⊢ χ
Theorem	ecase3d 560	Deduction for elimination by cases.
⊢ (φ → (ψ → θ))    &   ⊢ (φ → (χ → θ))    &   ⊢ (φ → (¬ (ψ ∨ χ) → θ))    ⇒   ⊢ (φ → θ)
Theorem	caselem 561	Lemma for combining cases.
⊢ (((φ ∨ ψ) ∧ (χ ∨ θ)) ↔ (((φ ∧ χ) ∨ (ψ ∧ χ)) ∨ ((φ ∧ θ) ∨ (ψ ∧ θ))))
Theorem	ccase 562	Inference for combining cases.
⊢ ((φ ∧ ψ) → τ)    &   ⊢ ((χ ∧ ψ) → τ)    &   ⊢ ((φ ∧ θ) → τ)    &   ⊢ ((χ ∧ θ) → τ)    ⇒   ⊢ (((φ ∨ χ) ∧ (ψ ∨ θ)) → τ)
Theorem	ccased 563	Deduction for combining cases.
⊢ (φ → ((ψ ∧ χ) → η))    &   ⊢ (φ → ((θ ∧ χ) → η))    &   ⊢ (φ → ((ψ ∧ τ) → η))    &   ⊢ (φ → ((θ ∧ τ) → η))    ⇒   ⊢ (φ → (((ψ ∨ θ) ∧ (χ ∨ τ)) → η))
Theorem	ccase2 564	Inference for combining cases.
⊢ ((φ ∧ ψ) → τ)    &   ⊢ (χ → τ)    &   ⊢ (θ → τ)    ⇒   ⊢ (((φ ∨ χ) ∧ (ψ ∨ θ)) → τ)
Theorem	4cases 565	Inference eliminating two antecedents from the four possible cases that result from their true/false combinations.
⊢ ((φ ∧ ψ) → χ)    &   ⊢ ((φ ∧ ¬ ψ) → χ)    &   ⊢ ((¬ φ ∧ ψ) → χ)    &   ⊢ ((¬ φ ∧ ¬ ψ) → χ)    ⇒   ⊢ χ
Theorem	niabn 566	Miscellaneous inference relating falsehoods.
⊢ φ    ⇒   ⊢ (¬ ψ → ((χ ∧ ψ) ↔ ¬ φ))
Theorem	dedlem0a 567	Lemma for an alternate version of weak deduction theorem.
⊢ (φ → (ψ ↔ ((χ → φ) → (ψ ∧ φ))))
Theorem	dedlem0b 568	Lemma for an alternate version of weak deduction theorem.
⊢ (¬ φ → (ψ ↔ ((ψ → φ) → (χ ∧ φ))))
Theorem	dedlema 569	Lemma for weak deduction theorem.
⊢ (φ → (ψ ↔ ((ψ ∧ φ) ∨ (χ ∧ ¬ φ))))
Theorem	dedlemb 570	Lemma for weak deduction theorem.
⊢ (¬ φ → (χ ↔ ((ψ ∧ φ) ∨ (χ ∧ ¬ φ))))
Theorem	elimh 571	Hypothesis builder for weak deduction theorem. For more information, see the Deduction Theorem link on the Metamath Proof Explorer home page.
⊢ ((φ ↔ ((φ ∧ χ) ∨ (ψ ∧ ¬ χ))) → (χ ↔ τ))    &   ⊢ ((ψ ↔ ((φ ∧ χ) ∨ (ψ ∧ ¬ χ))) → (θ ↔ τ))    &   ⊢ θ    ⇒   ⊢ τ
Theorem	dedt 572	The weak deduction theorem. For more information, see the Deduction Theorem link on the Metamath Proof Explorer home page.
⊢ ((φ ↔ ((φ ∧ χ) ∨ (ψ ∧ ¬ χ))) → (θ ↔ τ))    &   ⊢ τ    ⇒   ⊢ (χ → θ)
Theorem	con3th 573	Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. This version of con3 86 demonstrates the use of the weak deduction theorem to derive it from con3i 90.
⊢ ((φ → ψ) → (¬ ψ → ¬ φ))
Theorem	consensus 574	The consensus theorem. This theorem and its dual (with ∨ and ∧ interchanged) are commonly used in computer logic design to eliminate redundant terms from Boolean expressions. Specifically, we show the term (ψ ∧ χ) on the left-hand side is redundant.
⊢ ((((φ ∧ ψ) ∨ (¬ φ ∧ χ)) ∨ (ψ ∧ χ)) ↔ ((φ ∧ ψ) ∨ (¬ φ ∧ χ)))
Theorem	ninba 575	Miscellaneous inference relating falsehoods.
⊢ φ    ⇒   ⊢ (¬ ψ → (¬ φ ↔ (χ ∧ ψ)))
Theorem	prlem1 576	A specialized lemma for set theory (axiom of pairing).
⊢ (φ → (η ↔ χ))    &   ⊢ (ψ → ¬ θ)    ⇒   ⊢ (φ → (ψ → (((ψ ∧ χ) ∨ (θ ∧ τ)) → η)))
Theorem	prlem2 577	A specialized lemma for set theory (axiom of pairing).
⊢ (((φ ∧ ψ) ∨ (χ ∧ θ)) ↔ ((φ ∨ χ) ∧ ((φ ∧ ψ) ∨ (χ ∧ θ))))
Theorem	oplem1 578	A specialized lemma for set theory (ordered pair theorem).
⊢ (φ → (ψ ∨ χ))    &   ⊢ (φ → (θ ∨ τ))    &   ⊢ (ψ ↔ θ)    &   ⊢ (χ → (θ ↔ τ))    ⇒   ⊢ (φ → ψ)
Theorem	rnlem 579	Lemma used in construction of real numbers.
⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) ↔ (((φ ∧ χ) ∧ (ψ ∧ θ)) ∧ ((φ ∧ θ) ∧ (ψ ∧ χ))))
Syntax	w3o 580	Extend wff definition to include 3-way disjunction ('or').
wff (φ ∨ ψ ∨ χ)
Syntax	w3a 581	Extend wff definition to include 3-way conjunction ('and').
wff (φ ∧ ψ ∧ χ)
Definition	df-3or 582	Define disjunction ('or') of 3 wff's. Definition *2.33 of [WhiteheadRussell] p. 105. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law orass 218.
⊢ ((φ ∨ ψ ∨ χ) ↔ ((φ ∨ ψ) ∨ χ))
Definition	df-3an 583	Define conjunction ('and') of 3 wff.s. Definition *4.34 of [WhiteheadRussell] p. 118. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law anass 336.
⊢ ((φ ∧ ψ ∧ χ) ↔ ((φ ∧ ψ) ∧ χ))
Theorem	3orass 584	Associative law for triple disjunction.
⊢ ((φ ∨ ψ ∨ χ) ↔ (φ ∨ (ψ ∨ χ)))
Theorem	3anass 585	Associative law for triple conjunction.
⊢ ((φ ∧ ψ ∧ χ) ↔ (φ ∧ (ψ ∧ χ)))
Theorem	3anrot 586	Rotation law for triple conjunction.
⊢ ((φ ∧ ψ ∧ χ) ↔ (ψ ∧ χ ∧ φ))
Theorem	3orrot 587	Rotation law for triple disjunction.
⊢ ((φ ∨ ψ ∨ χ) ↔ (ψ ∨ χ ∨ φ))
Theorem	3ancoma 588	Commutation law for triple conjunction.
⊢ ((φ ∧ ψ ∧ χ) ↔ (ψ ∧ φ ∧ χ))
Theorem	3ancomb 589	Commutation law for triple conjunction.
⊢ ((φ ∧ ψ ∧ χ) ↔ (φ ∧ χ ∧ ψ))
Theorem	3anrev 590	Reversal law for triple conjunction.
⊢ ((φ ∧ ψ ∧ χ) ↔ (χ ∧ ψ ∧ φ))
Theorem	3simpa 591	Simplification of triple conjunction.
⊢ ((φ ∧ ψ ∧ χ) → (φ ∧ ψ))
Theorem	3simpb 592	Simplification of triple conjunction.
⊢ ((φ ∧ ψ ∧ χ) → (φ ∧ χ))
Theorem	3simpc 593	Simplification of triple conjunction.
⊢ ((φ ∧ ψ ∧ χ) → (ψ ∧ χ))
Theorem	3simp1 594	Simplification of triple conjunction.
⊢ ((φ ∧ ψ ∧ χ) → φ)
Theorem	3simp2 595	Simplification of triple conjunction.
⊢ ((φ ∧ ψ ∧ χ) → ψ)
Theorem	3simp3 596	Simplification of triple conjunction.
⊢ ((φ ∧ ψ ∧ χ) → χ)
Theorem	3adant1 597	Deduction adding a conjunct to an antecedent.
⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ ((θ ∧ φ ∧ ψ) → χ)
Theorem	3adant2 598	Deduction adding a conjunct to an antecedent.
⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ ((φ ∧ θ ∧ ψ) → χ)
Theorem	3adant3 599	Deduction adding a conjunct to an antecedent.
⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ ((φ ∧ ψ ∧ θ) → χ)
Theorem	3mix1 600	Introduction in triple disjunction.
⊢ (φ → (φ ∨ ψ ∨ χ))