Metamath Proof Explorer - mmtheorems

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 - 1-100 - Page 1 of 58

Type	Label	Description
Statement
Syntax	wn 1	If φ is a wff, so is ¬ φ or "not φ". Part of the recursive definition of a wff (well-formed formula). In classical logic (which is our logic), a wff is interpreted as either true or false. So if φ is true, then ¬ φ is false; if φ is false, then ¬ φ is true. Traditionally, Greek letters are used to represent wffs, and we follow this convention. In propositional calculus, we define only wffs built up from other wffs, i.e. there is no starting or "atomic" wff. Later, in predicate calculus, we will extend the basic wff definition by including atomic wffs (weq 797 and wel 803).
wff ¬ φ
Syntax	wi 2	If φ and ψ are wff's, so is (φ → ψ) or "φ implies ψ." Part of the recursive definition of a wff. The resulting wff is (interpreted as) false when φ is true and ψ is false; it is true otherwise. (Think of the truth table for an OR gate with input φ connected through an inverter.) The left-hand wff is called the antecedent, and the right-hand wff is called the consequent. In the case of (φ → (ψ → χ)), the middle ψ may be informally called either an antecedent or part of the consequent depending on context.
wff (φ → ψ)
Axiom	ax-1 3	Axiom Simp. Axiom A1 of [Margaris] p. 49. One of the 3 axioms of propositional calculus. The 3 axioms are also given as Definition 2.1 of [Hamilton] p. 28. This axiom is called Simp or "the principle of simplification" in Principia Mathematica (Theorem *2.02 of [WhiteheadRussell] p. 100) because "it enables us to pass from the joint assertion of φ and ψ to the assertion of φ simply." Propositional calculus (axioms ax-1 3 through ax-3 5 and rule ax-mp 6) can be thought of as asserting formulas that are universally "true" when their variables are replaced by any combination of "true" and "false". Propositional calculus was first formalized by Frege in 1879, using as his axioms (in addition to rule ax-mp 6) the wffs ax-1 3, ax-2 4, pm2.04 31, con3 86, nega 78, and negb 79. Around 1930, Lukasiewicz simplified the system by eliminating the third (which follows from the first two, as you can see by looking at the proof of pm2.04 31) and replacing the last three with our ax-3 5. (Thanks to Ted Ulrich for this information.) The theorems of propositional calculus are also called tautologies. Tautologies can be proved very simply using truth tables, based on the true/false interpretation of propositional calculus. This is called the semantic approach. Our approach is called the syntactic approach, in which everything is derived from axioms. A metatheorem called the Completeness Theorem for Propositional Calculus shows that the two approaches are equivalent and even provides an algorithm for automatically generating syntactic proofs from a truth table. Those proofs, however, tend to be long, and the much shorter proofs that we show here were found manually.
⊢ (φ → (ψ → φ))
Axiom	ax-2 4	Axiom Frege. Axiom A2 of [Margaris] p. 49. One of the 3 axioms of propositional calculus. It distributes an antecedent over two consequents. This axiom was part of Frege's original system and is known as Frege in the literature. It is also proved as Theorem *2.77 of [WhiteheadRussell] p. 108.
⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)))
Axiom	ax-3 5	Axiom Transp. Axiom A3 of [Margaris] p. 49. One of the 3 axioms of propositional calculus. It swaps or transposes the order of the consequents when negation is removed. An informal example is that the statement "if there are no clouds in the sky, it is not raining" implies the statement "if it is raining, there are clouds in the sky." This axiom is called Transp or "the principle of transposition" in Principia Mathematica (Theorem *2.17 of [WhiteheadRussell] p. 103).
⊢ ((¬ φ → ¬ ψ) → (ψ → φ))
Axiom	ax-mp 6	Rule of Modus Ponens. The postulated inference rule of propositional calculus. See e.g. Rule 1 of [Hamilton] p. 73. The rule says, "if φ is true, and φ implies ψ, then ψ must also be true." This rule is sometimes called "detachment", since it detaches the minor premise from the major premise.
⊢ φ    &   ⊢ (φ → ψ)    ⇒   ⊢ ψ
Theorem	a1i 7	Inference derived from axiom ax-1 3. See a1d 14 for an explanation of our informal use of the terms "inference" and "deduction".
⊢ φ    ⇒   ⊢ (ψ → φ)
Theorem	a2i 8	Inference derived from axiom ax-2 4.
⊢ (φ → (ψ → χ))    ⇒   ⊢ ((φ → ψ) → (φ → χ))
Theorem	id 9	Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see id1 10.
⊢ (φ → φ)
Theorem	id1 10	Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. This version is proved directly from the axioms for demonstration purposes. This proof is identical, step for step, to the proofs of Theorem 1 of [Margaris] p. 51 and Example 2.7(a) of [Hamilton] p. 31. For a shorter version of the proof that takes advantage of a previously proved inference, see id 9.
⊢ (φ → φ)
Theorem	idd 11	Principle of identity with antecedent.
⊢ (φ → (ψ → ψ))
Theorem	syl 12	Syllogism inference. (A bit of trivia: this is the most commonly referenced assertion in our database. In second place is ax-mp 6, followed by visset 1350, bitr 151, imp 277, and exp 291. The Metamath program command 'show usage' shows the number of references.)
⊢ (φ → ψ)    &   ⊢ (ψ → χ)    ⇒   ⊢ (φ → χ)
Theorem	com12 13	Inference that swaps (commutes) antecedents in an implication.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (ψ → (φ → χ))
Theorem	a1d 14	Deduction introducing an embedded antecedent. Naming convention: We often call a theorem a "deduction" and suffix its label with "d" whenever the hypotheses and conclusion are each prefixed with the same antecedent. This allows us to use the theorem in places where (in traditional textbook formalizations) the standard Deduction Theorem would be used; here φ would be replaced with a conjunction (df-an 198) of the hypotheses of the would-be deduction. By contrast, we tend to call the simpler version with no common antecedent an "inference" and suffix its label with "i"; compare theorem a1i 7. Finally, a "theorem" would be the form with no hypotheses; in this case the "theorem" form would be the original axiom ax-1 3. In propositional calculus we usually prove the theorem form first without a suffix on its label (e.g. pm2.43 57 vs. pm2.43i 58 vs. pm2.43d 59), but (much) later we often suffix the theorem form's label with "t" as in negnegt 4157 vs. negneg 4154, especially when our "weak deduction theorem" dedth 1784 is used to prove the theorem form from its inference form. When an inference is converted to a theorem by eliminating an "is a set" hypothesis, we sometimes suffix the theorem form with "g" (for somewhat misnamed "generalized") as in uniex 1947 vs. uniexg 1948.
⊢ (φ → ψ)    ⇒   ⊢ (φ → (χ → ψ))
Theorem	a2d 15	Deduction distributing an embedded antecedent.
⊢ (φ → (ψ → (χ → θ)))    ⇒   ⊢ (φ → ((ψ → χ) → (ψ → θ)))
Theorem	syl1 16	A closed form of syllogism. Theorem *2.05 of [WhiteheadRussell] p. 100.
⊢ ((φ → ψ) → ((χ → φ) → (χ → ψ)))
Theorem	syl2 17	A closed form of syllogism. Theorem *2.06 of [WhiteheadRussell] p. 100.
⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ)))
Theorem	syl3 18	Inference adding common antecedents in an implication.
⊢ (φ → ψ)    ⇒   ⊢ ((χ → φ) → (χ → ψ))
Theorem	syl4 19	Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent.
⊢ (φ → ψ)    ⇒   ⊢ ((ψ → χ) → (φ → χ))
Theorem	syl34 20	Inference joining two implications.
⊢ (φ → ψ)    &   ⊢ (χ → θ)    ⇒   ⊢ ((ψ → χ) → (φ → θ))
Theorem	3syl 21	Inference chaining two syllogisms.
⊢ (φ → ψ)    &   ⊢ (ψ → χ)    &   ⊢ (χ → θ)    ⇒   ⊢ (φ → θ)
Theorem	syl5 22	A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise.
⊢ (φ → (ψ → χ))    &   ⊢ (θ → ψ)    ⇒   ⊢ (φ → (θ → χ))
Theorem	syl6 23	A syllogism rule of inference. The second premise is used to replace the consequent of the first premise.
⊢ (φ → (ψ → χ))    &   ⊢ (χ → θ)    ⇒   ⊢ (φ → (ψ → θ))
Theorem	syl7 24	A syllogism rule of inference. The second premise is used to replace the third antecedent of the first premise.
⊢ (φ → (ψ → (χ → θ)))    &   ⊢ (τ → χ)    ⇒   ⊢ (φ → (ψ → (τ → θ)))
Theorem	syl8 25	A syllogism rule of inference. The second premise is used to replace the consequent of the first premise.
⊢ (φ → (ψ → (χ → θ)))    &   ⊢ (θ → τ)    ⇒   ⊢ (φ → (ψ → (χ → τ)))
Theorem	syl3d 26	Deduction adding nested antecedents.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → ((θ → ψ) → (θ → χ)))
Theorem	syld 27	Syllogism deduction. (The proof was shortened by Mel L. O'Cat, 7-Aug-04.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (χ → θ))    ⇒   ⊢ (φ → (ψ → θ))
Theorem	syl4d 28	Deduction adding nested consequents.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → ((χ → θ) → (ψ → θ)))
Theorem	syl34d 29	Deduction combining antecedents and consequents.
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (θ → τ))    ⇒   ⊢ (φ → ((χ → θ) → (ψ → τ)))
Theorem	pm2.27 30	This theorem, called "Assertion," can be thought of as closed form of modus ponens. Theorem *2.27 of [WhiteheadRussell] p. 104.
⊢ (φ → ((φ → ψ) → ψ))
Theorem	pm2.04 31	Swap antecedents. Theorem *2.04 of [WhiteheadRussell] p. 100.
⊢ ((φ → (ψ → χ)) → (ψ → (φ → χ)))
Theorem	com23 32	Commutation of antecedents. Swap 2nd and 3rd.
⊢ (φ → (ψ → (χ → θ)))    ⇒   ⊢ (φ → (χ → (ψ → θ)))
Theorem	com13 33	Commutation of antecedents. Swap 1st and 3rd.
⊢ (φ → (ψ → (χ → θ)))    ⇒   ⊢ (χ → (ψ → (φ → θ)))
Theorem	com3l 34	Commutation of antecedents. Rotate left.
⊢ (φ → (ψ → (χ → θ)))    ⇒   ⊢ (ψ → (χ → (φ → θ)))
Theorem	com3r 35	Commutation of antecedents. Rotate right.
⊢ (φ → (ψ → (χ → θ)))    ⇒   ⊢ (χ → (φ → (ψ → θ)))
Theorem	com34 36	Commutation of antecedents. Swap 3rd and 4th.
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ (φ → (ψ → (θ → (χ → τ))))
Theorem	com24 37	Commutation of antecedents. Swap 2nd and 4th.
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ (φ → (θ → (χ → (ψ → τ))))
Theorem	com14 38	Commutation of antecedents. Swap 1st and 4th.
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ (θ → (ψ → (χ → (φ → τ))))
Theorem	com4l 39	Commutation of antecedents. Rotate left. (The proof was shortened by Mel L. O'Cat, 15-Aug-04.)
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ (ψ → (χ → (θ → (φ → τ))))
Theorem	com4t 40	Commutation of antecedents. Rotate twice.
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ (χ → (θ → (φ → (ψ → τ))))
Theorem	com4r 41	Commutation of antecedents. Rotate right.
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ (θ → (φ → (ψ → (χ → τ))))
Theorem	a1dd 42	Deduction introducing a nested embedded antecedent.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (ψ → (θ → χ)))
Theorem	mp2 43	A double modus ponens inference.
⊢ φ    &   ⊢ ψ    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ χ
Theorem	mpi 44	A nested modus ponens inference.
⊢ ψ    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → χ)
Theorem	mpii 45	A doubly nested modus ponens inference.
⊢ χ    &   ⊢ (φ → (ψ → (χ → θ)))    ⇒   ⊢ (φ → (ψ → θ))
Theorem	mpd 46	A modus ponens deduction.
⊢ (φ → ψ)    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → χ)
Theorem	mpdd 47	A nested modus ponens deduction.
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (ψ → (χ → θ)))    ⇒   ⊢ (φ → (ψ → θ))
Theorem	mpid 48	A nested modus ponens deduction.
⊢ (φ → χ)    &   ⊢ (φ → (ψ → (χ → θ)))    ⇒   ⊢ (φ → (ψ → θ))
Theorem	mpcom 49	Modus ponens inference with commutation of antecedents.
⊢ (ψ → φ)    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (ψ → χ)
Theorem	syldd 50	Nested syllogism deduction.
⊢ (φ → (ψ → (χ → θ)))    &   ⊢ (φ → (ψ → (θ → τ)))    ⇒   ⊢ (φ → (ψ → (χ → τ)))
Theorem	sylcom 51	Syllogism inference with commutation of antecedents.
⊢ (φ → (ψ → χ))    &   ⊢ (ψ → (χ → θ))    ⇒   ⊢ (φ → (ψ → θ))
Theorem	syli 52	Syllogism inference with common nested antecedent.
⊢ (ψ → (φ → χ))    &   ⊢ (χ → (φ → θ))    ⇒   ⊢ (ψ → (φ → θ))
Theorem	syl5d 53	A nested syllogism deduction. (The proof was shortened by Josh Purinton, 29-Dec-00.)
⊢ (φ → (ψ → (χ → θ)))    &   ⊢ (φ → (τ → χ))    ⇒   ⊢ (φ → (ψ → (τ → θ)))
Theorem	syl6d 54	A nested syllogism deduction. (The proof was shortened by Josh Purinton, 29-Dec-00.)
⊢ (φ → (ψ → (χ → θ)))    &   ⊢ (φ → (θ → τ))    ⇒   ⊢ (φ → (ψ → (χ → τ)))
Theorem	syl9 55	A nested syllogism inference with different antecedents. (The proof was shortened by Josh Purinton, 29-Dec-00.)
⊢ (φ → (ψ → χ))    &   ⊢ (θ → (χ → τ))    ⇒   ⊢ (φ → (θ → (ψ → τ)))
Theorem	syl9r 56	A nested syllogism inference with different antecedents.
⊢ (φ → (ψ → χ))    &   ⊢ (θ → (χ → τ))    ⇒   ⊢ (θ → (φ → (ψ → τ)))
Theorem	pm2.43 57	Absorption of redundant antecedent. Also called the "Contraction" or "Hilbert" axiom. Theorem *2.43 of [WhiteheadRussell] p. 106. (The proof was shortened by Mel L. O'Cat, 15-Aug-04.)
⊢ ((φ → (φ → ψ)) → (φ → ψ))
Theorem	pm2.43i 58	Inference absorbing redundant antecedent.
⊢ (φ → (φ → ψ))    ⇒   ⊢ (φ → ψ)
Theorem	pm2.43d 59	Deduction absorbing redundant antecedent.
⊢ (φ → (ψ → (ψ → χ)))    ⇒   ⊢ (φ → (ψ → χ))
Theorem	pm2.43a 60	Inference absorbing redundant antecedent.
⊢ (ψ → (φ → (ψ → χ)))    ⇒   ⊢ (ψ → (φ → χ))
Theorem	pm2.43b 61	Inference absorbing redundant antecedent.
⊢ (ψ → (φ → (ψ → χ)))    ⇒   ⊢ (φ → (ψ → χ))
Theorem	sylc 62	A syllogism inference combined with contraction.
⊢ (φ → (ψ → χ))    &   ⊢ (θ → φ)    &   ⊢ (θ → ψ)    ⇒   ⊢ (θ → χ)
Theorem	pm2.86 63	Converse of axiom ax-2 4. Theorem *2.86 of [WhiteheadRussell] p. 108.
⊢ (((φ → ψ) → (φ → χ)) → (φ → (ψ → χ)))
Theorem	pm2.86i 64	Inference based on pm2.86 63.
⊢ ((φ → ψ) → (φ → χ))    ⇒   ⊢ (φ → (ψ → χ))
Theorem	pm2.86d 65	Deduction based on pm2.86 63.
⊢ (φ → ((ψ → χ) → (ψ → θ)))    ⇒   ⊢ (φ → (ψ → (χ → θ)))
Theorem	loolin 66	The Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. (Contributed by Mel L. O'Cat, 12-Aug-04.)
⊢ (((φ → ψ) → (ψ → φ)) → (ψ → φ))
Theorem	loowoz 67	An alternate for the Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz, due to Barbara Wozniakowska, Reports on Mathematical Logic 10, 129-137 (1978). (Contributed by Mel L. O'Cat, 8-Aug-04.)
⊢ (((φ → ψ) → (φ → χ)) → ((ψ → φ) → (ψ → χ)))
Theorem	a3i 69	Inference rule derived from axiom ax-3 5.
⊢ (¬ φ → ¬ ψ)    ⇒   ⊢ (ψ → φ)
Theorem	a3d 70	Deduction derived from axiom ax-3 5.
⊢ (φ → (¬ ψ → ¬ χ))    ⇒   ⊢ (φ → (χ → ψ))
Theorem	pm2.21 71	From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law.
⊢ (¬ φ → (φ → ψ))
Theorem	pm2.24 72	Theorem *2.24 of [WhiteheadRussell] p. 104.
⊢ (φ → (¬ φ → ψ))
Theorem	pm2.21i 73	A contradiction implies anything. Inference from pm2.21 71.
⊢ ¬ φ    ⇒   ⊢ (φ → ψ)
Theorem	pm2.21d 74	A contradiction implies anything. Deduction from pm2.21 71.
⊢ (φ → ¬ ψ)    ⇒   ⊢ (φ → (ψ → χ))
Theorem	pm2.18 75	Proof by contradiction. Theorem *2.18 of [WhiteheadRussell] p. 103. Also called the Law of Clavius.
⊢ ((¬ φ → φ) → φ)
Theorem	peirce 76	Peirce's axiom. This odd-looking theorem is the "difference" between an intuitionistic system of propositional calculus and a classical system and is not accepted by intuitionists. When Peirce's axiom is added to an intuitionistic system, the system becomes equivalent to our classical system ax-1 3 through ax-3 5. A curious fact about this theorem is that it requires ax-3 5 for its proof even though the result has no negations in it.
⊢ (((φ → ψ) → φ) → φ)
Theorem	looinv 77	The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. Using dfor2 199, we can see that this essentially expresses "disjunction commutes." Theorem *2.69 of [WhiteheadRussell] p. 108.
⊢ (((φ → ψ) → ψ) → ((ψ → φ) → φ))
Theorem	nega 78	Double negation. Theorem *2.14 of [WhiteheadRussell] p. 102. (The proof was shortened by David Harvey, 5-Sep-99. An even shorter proof found by Josh Purinton, 29-Dec-00.)
⊢ (¬ ¬ φ → φ)
Theorem	negb 79	Converse of double negation. Theorem *2.12 of [WhiteheadRussell] p. 101.
⊢ (φ → ¬ ¬ φ)
Theorem	pm2.01 80	Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100.
⊢ ((φ → ¬ φ) → ¬ φ)
Theorem	pm2.01d 81	Deduction based on reductio ad absurdum.
⊢ (φ → (ψ → ¬ ψ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	con2 82	Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100.
⊢ ((φ → ¬ ψ) → (ψ → ¬ φ))
Theorem	con2d 83	A contraposition deduction.
⊢ (φ → (ψ → ¬ χ))    ⇒   ⊢ (φ → (χ → ¬ ψ))
Theorem	con1 84	Contraposition. Theorem *2.15 of [WhiteheadRussell] p. 102.
⊢ ((¬ φ → ψ) → (¬ ψ → φ))
Theorem	con1d 85	A contraposition deduction.
⊢ (φ → (¬ ψ → χ))    ⇒   ⊢ (φ → (¬ χ → ψ))
Theorem	con3 86	Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103.
⊢ ((φ → ψ) → (¬ ψ → ¬ φ))
Theorem	con3d 87	A contraposition deduction.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (¬ χ → ¬ ψ))
Theorem	con1i 88	A contraposition inference.
⊢ (¬ φ → ψ)    ⇒   ⊢ (¬ ψ → φ)
Theorem	con2i 89	A contraposition inference.
⊢ (φ → ¬ ψ)    ⇒   ⊢ (ψ → ¬ φ)
Theorem	con3i 90	A contraposition inference.
⊢ (φ → ψ)    ⇒   ⊢ (¬ ψ → ¬ φ)
Theorem	pm2.36 91	Theorem *2.36 of [WhiteheadRussell] p. 105.
⊢ ((ψ → χ) → ((¬ φ → ψ) → (¬ χ → φ)))
Theorem	pm2.21ni 92	Inference related to pm2.21 71.
⊢ φ    ⇒   ⊢ (¬ φ → ψ)
Theorem	mto 93	The rule of modus tollens.
⊢ ¬ ψ    &   ⊢ (φ → ψ)    ⇒   ⊢ ¬ φ
Theorem	mtoi 94	Modus tollens inference.
⊢ ¬ χ    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	mtod 95	Modus tollens deduction.
⊢ (φ → ¬ χ)    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	mt2 96	A rule similar to modus tollens.
⊢ ψ    &   ⊢ (φ → ¬ ψ)    ⇒   ⊢ ¬ φ
Theorem	mt2i 97	Modus tollens inference.
⊢ χ    &   ⊢ (φ → (ψ → ¬ χ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	mt2d 98	Modus tollens deduction.
⊢ (φ → χ)    &   ⊢ (φ → (ψ → ¬ χ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	mt3 99	A rule similar to modus tollens.
⊢ ¬ ψ    &   ⊢ (¬ φ → ψ)    ⇒   ⊢ φ
Theorem	mt3i 100	Modus tollens inference.
⊢ ¬ χ    &   ⊢ (φ → (¬ ψ → χ))    ⇒   ⊢ (φ → ψ)