Metamath Proof Explorer - mmtheorems2

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 - 101-200 - Page 2 of 58

Type	Label	Description
Statement
Theorem	mt3d 101	Modus tollens deduction.
|- (ph -> -. ch)   &   |- (ph -> (-. ps -> ch))   =>   |- (ph -> ps)
Theorem	nsyl 102	A negated syllogism inference.
|- (ph -> -. ps)   &   |- (ch -> ps)   =>   |- (ph -> -. ch)
Theorem	nsyl2 103	A negated syllogism inference.
|- (ph -> -. ps)   &   |- (-. ch -> ps)   =>   |- (ph -> ch)
Theorem	nsyl3 104	A negated syllogism inference.
|- (ph -> -. ps)   &   |- (ch -> ps)   =>   |- (ch -> -. ph)
Theorem	nsyl4 105	A negated syllogism inference.
|- (ph -> ps)   &   |- (-. ph -> ch)   =>   |- (-. ch -> ps)
Theorem	nsyli 106	A negated syllogism inference.
|- (ph -> (ps -> ch))   &   |- (th -> -. ch)   =>   |- (ph -> (th -> -. ps))
Theorem	pm3.2im 107	Theorem *3.2 of [WhiteheadRussell] p. 111, expressed with primitive connectives. (The proof was shortened by Josh Purinton, 29-Dec-00.)
|- (ph -> (ps -> -. (ph -> -. ps)))
Theorem	mth8 108	Theorem 8 of [Margaris] p. 60. (The proof was shortened by Josh Purinton, 29-Dec-00.)
|- (ph -> (-. ps -> -. (ph -> ps)))
Theorem	pm2.61 109	Theorem *2.61 of [WhiteheadRussell] p. 107. Useful for eliminating an antecedent.
|- ((ph -> ps) -> ((-. ph -> ps) -> ps))
Theorem	pm2.61i 110	Inference eliminating an antecedent.
|- (ph -> ps)   &   |- (-. ph -> ps)   =>   |- ps
Theorem	pm2.61d2 111	Inference eliminating an antecedent.
|- (ph -> (-. ps -> ch))   &   |- (ps -> ch)   =>   |- (ph -> ch)
Theorem	pm2.61d 112	Deduction eliminating an antecedent.
|- (ph -> (ps -> ch))   &   |- (ph -> (-. ps -> ch))   =>   |- (ph -> ch)
Theorem	pm2.61ii 113	Inference eliminating two antecedents. (The proof was shortened by Josh Purinton, 29-Dec-00.)
|- (-. ph -> (-. ps -> ch))   &   |- (ph -> ch)   &   |- (ps -> ch)   =>   |- ch
Theorem	pm2.61iii 114	Inference eliminating three antecedents.
|- (-. ph -> (-. ps -> (-. ch -> th)))   &   |- (ph -> th)   &   |- (ps -> th)   &   |- (ch -> th)   =>   |- th
Theorem	pm2.65 115	Theorem *2.65 of [WhiteheadRussell] p. 107. Useful for eliminating a consequent.
|- ((ph -> ps) -> ((ph -> -. ps) -> -. ph))
Theorem	pm2.65i 116	Inference rule for proof by contradiction.
|- (ph -> ps)   &   |- (ph -> -. ps)   =>   |- -. ph
Theorem	pm2.65d 117	Deduction rule for proof by contradiction.
|- (ph -> (ps -> ch))   &   |- (ph -> (ps -> -. ch))   =>   |- (ph -> -. ps)
Theorem	ja 118	Inference joining the antecedents of two premises. (The proof was shortened by Mel L. O'Cat, 30-Aug-04.)
|- (-. ph -> ch)   &   |- (ps -> ch)   =>   |- ((ph -> ps) -> ch)
Theorem	jc 119	Inference joining the consequents of two premises.
|- (ph -> ps)   &   |- (ph -> ch)   =>   |- (ph -> -. (ps -> -. ch))
Theorem	pm3.26im 120	Simplification. Similar to Theorem *3.26 of [WhiteheadRussell] p. 112.
|- (-. (ph -> -. ps) -> ph)
Theorem	pm3.27im 121	Simplification. Similar to Theorem *3.27 of [WhiteheadRussell] p. 112.
|- (-. (ph -> -. ps) -> ps)
Theorem	impt 122	Importation theorem expressed with primitive connectives.
|- ((ph -> (ps -> ch)) -> (-. (ph -> -. ps) -> ch))
Theorem	expt 123	Exportation theorem expressed with primitive connectives.
|- ((-. (ph -> -. ps) -> ch) -> (ph -> (ps -> ch)))
Theorem	impi 124	An importation inference.
|- (ph -> (ps -> ch))   =>   |- (-. (ph -> -. ps) -> ch)
Theorem	expi 125	An exportation inference.
|- (-. (ph -> -. ps) -> ch)   =>   |- (ph -> (ps -> ch))
Theorem	bijust 126	Theorem used to justify definition of biconditional df-bi 128. (The proof was shortened by Josh Purinton, 29-Dec-00.)
|- -. ((ph -> ph) -> -. (ph -> ph))
Syntax	wb 127	Extend our wff definition to include the biconditional connective.
wff (ph <-> ps)
Definition	df-bi 128	This is our first definition, which defines the biconditional connective <->. Unlike most traditional developments, we have chosen not to have a separate symbol such as 'Df.' to mean 'is defined as.' Instead, we will later use the biconditional connective for this purpose, as it allows us to use logic to manipulate definitions directly (df-or 197 is its first use). Here we use the biconditional connective to define itself, a feat which requires a little care. We define (ph <-> ps) as -. ((ph -> ps) -> -. (ps -> ph)) but we don't yet have a notation that can express this directly, so we use a more complicated expression using the language that we have so far. The justification for our definition is that if we mechanically substitute the second wff for the first in the definition, the definition becomes an instance of previously proved theorem bijust 126. Note that from Metamath's point of view, a definition is just another axiom; but from our high level point of view, we are are not strengthening the language since if we mechanically eliminate the new symbol <-> we will not end up with any theorems we could not prove before. To indicate this fact we prefix definition labels with "df-" instead of "ax-". (This prefixing is an informal convention that means nothing to the Metamath proof verifier; it is just for human readability.) See bii 140 and bi 396 for theorems suggesting the typical textbook definition of <->.
|- -. (((ph <-> ps) -> -. ((ph -> ps) -> -. (ps -> ph))) -> -. (-. ((ph -> ps) -> -. (ps -> ph)) -> (ph <-> ps)))
Theorem	biigb 129	This proof of bii 140, discovered by Gregory Bush on 8-Mar-04, has several curious properties. First, it has only 17 steps directly from the axioms and df-bi 128, compared to over 800 steps were the proof of bii 140 expanded into axioms. Second, step 2 demands only the property of "true"; any axiom (or theorem) could be used. Third, it illustrates how intermediate steps can "blow up" in size even in short proofs. Fourth, the compressed proof is only 2.5 lines long, but the web page is over 200kB in size. If there were an obfuscated code contest for proofs, this might be a winner.
|- ((ph <-> ps) <-> -. ((ph -> ps) -> -. (ps -> ph)))
Theorem	bi1 130	Property of the biconditional connective.
|- ((ph <-> ps) -> (ph -> ps))
Theorem	bi2 131	Property of the biconditional connective.
|- ((ph <-> ps) -> (ps -> ph))
Theorem	bi3 132	Property of the biconditional connective.
|- ((ph -> ps) -> ((ps -> ph) -> (ph <-> ps)))
Theorem	biimp 133	Infer an implication from a logical equivalence.
|- (ph <-> ps)   =>   |- (ph -> ps)
Theorem	biimpr 134	Infer a converse implication from a logical equivalence.
|- (ph <-> ps)   =>   |- (ps -> ph)
Theorem	biimpd 135	Deduce an implication from a logical equivalence.
|- (ph -> (ps <-> ch))   =>   |- (ph -> (ps -> ch))
Theorem	biimprd 136	Deduce a converse implication from a logical equivalence.
|- (ph -> (ps <-> ch))   =>   |- (ph -> (ch -> ps))
Theorem	biimpcd 137	Deduce a commuted implication from a logical equivalence.
|- (ph -> (ps <-> ch))   =>   |- (ps -> (ph -> ch))
Theorem	biimprcd 138	Deduce a converse commuted implication from a logical equivalence.
|- (ph -> (ps <-> ch))   =>   |- (ch -> (ph -> ps))
Theorem	impbi 139	Infer an equivalence from an implication and its converse.
|- (ph -> ps)   &   |- (ps -> ph)   =>   |- (ph <-> ps)
Theorem	bii 140	Relate the biconditional connective to primitive connectives. See biigb 129 for an unusual version proved directly from axioms.
|- ((ph <-> ps) <-> -. ((ph -> ps) -> -. (ps -> ph)))
Theorem	bi2.04 141	Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122.
|- ((ph -> (ps -> ch)) <-> (ps -> (ph -> ch)))
Theorem	pm4.13 142	Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117.
|- (ph <-> -. -. ph)
Theorem	pm4.1 143	Contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116.
|- ((ph -> ps) <-> (-. ps -> -. ph))
Theorem	bi2.03 144	Contraposition. Bidirectional version of con2 82.
|- ((ph -> -. ps) <-> (ps -> -. ph))
Theorem	bi2.15 145	Contraposition. Bidirectional version of con1 84.
|- ((-. ph -> ps) <-> (-. ps -> ph))
Theorem	pm5.4 146	Antecedent absorption implication. Theorem *5.4 of [WhiteheadRussell] p. 125.
|- ((ph -> (ph -> ps)) <-> (ph -> ps))
Theorem	imdi 147	Distributive law for implication. Compare Theorem *5.41 of [WhiteheadRussell] p. 125.
|- ((ph -> (ps -> ch)) <-> ((ph -> ps) -> (ph -> ch)))
Theorem	pm4.2 148	Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117.
|- (ph <-> ph)
Theorem	pm4.2i 149	Principle of identity with antecedent.
|- (ph -> (ps <-> ps))
Theorem	bicomi 150	Inference from commutative law for logical equivalence.
|- (ph <-> ps)   =>   |- (ps <-> ph)
Theorem	bitr 151	An inference from transitive law for logical equivalence.
|- (ph <-> ps)   &   |- (ps <-> ch)   =>   |- (ph <-> ch)
Theorem	bitr2 152	An inference from transitive law for logical equivalence.
|- (ph <-> ps)   &   |- (ps <-> ch)   =>   |- (ch <-> ph)
Theorem	bitr3 153	An inference from transitive law for logical equivalence.
|- (ps <-> ph)   &   |- (ps <-> ch)   =>   |- (ph <-> ch)
Theorem	bitr4 154	An inference from transitive law for logical equivalence.
|- (ph <-> ps)   &   |- (ch <-> ps)   =>   |- (ph <-> ch)
Theorem	3bitr 155	A chained inference from transitive law for logical equivalence.
|- (ph <-> ps)   &   |- (ps <-> ch)   &   |- (ch <-> th)   =>   |- (ph <-> th)
Theorem	3bitr3 156	A chained inference from transitive law for logical equivalence.
|- (ph <-> ps)   &   |- (ph <-> ch)   &   |- (ps <-> th)   =>   |- (ch <-> th)
Theorem	3bitr3r 157	A chained inference from transitive law for logical equivalence.
|- (ph <-> ps)   &   |- (ph <-> ch)   &   |- (ps <-> th)   =>   |- (th <-> ch)
Theorem	3bitr4 158	A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence.
|- (ph <-> ps)   &   |- (ch <-> ph)   &   |- (th <-> ps)   =>   |- (ch <-> th)
Theorem	3bitr4r 159	A chained inference from transitive law for logical equivalence.
|- (ph <-> ps)   &   |- (ch <-> ph)   &   |- (th <-> ps)   =>   |- (th <-> ch)
Theorem	imbi2i 160	Introduce an antecedent to both sides of a logical equivalence.
|- (ph <-> ps)   =>   |- ((ch -> ph) <-> (ch -> ps))
Theorem	imbi1i 161	Introduce a consequent to both sides of a logical equivalence.
|- (ph <-> ps)   =>   |- ((ph -> ch) <-> (ps -> ch))
Theorem	negbii 162	Negate both sides of a logical equivalence.
|- (ph <-> ps)   =>   |- (-. ph <-> -. ps)
Theorem	imbi12i 163	Join two logical equivalences to form equivalence of implications.
|- (ph <-> ps)   &   |- (ch <-> th)   =>   |- ((ph -> ch) <-> (ps -> th))
Theorem	mpbi 164	An inference from a biconditional, related to modus ponens.
|- ph   &   |- (ph <-> ps)   =>   |- ps
Theorem	mpbir 165	An inference from a biconditional, related to modus ponens.
|- ps   &   |- (ph <-> ps)   =>   |- ph
Theorem	mtbi 166	An inference from a biconditional, related to modus tollens.
|- -. ph   &   |- (ph <-> ps)   =>   |- -. ps
Theorem	mtbir 167	An inference from a biconditional, related to modus tollens.
|- -. ps   &   |- (ph <-> ps)   =>   |- -. ph
Theorem	mpbii 168	An inference from a nested biconditional, related to modus ponens.
|- ps   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> ch)
Theorem	mpbiri 169	An inference from a nested biconditional, related to modus ponens.
|- ch   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> ps)
Theorem	mpbid 170	A deduction from a biconditional, related to modus ponens.
|- (ph -> ps)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> ch)
Theorem	mpbird 171	A deduction from a biconditional, related to modus ponens.
|- (ph -> ch)   &   |- (ph -> (ps <-> ch))   =>   |-