P. 2 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 101-200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	com15 101	Commutation of antecedents. Swap 1st and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) (Proof shortened by Wolf Lammen, 29-Jul-2012.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (𝜏 → (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜂)))))
Theorem	com52l 102	Commutation of antecedents. Rotate left twice. (Contributed by Jeff Hankins, 28-Jun-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (𝜒 → (𝜃 → (𝜏 → (𝜑 → (𝜓 → 𝜂)))))
Theorem	com52r 103	Commutation of antecedents. Rotate right twice. (Contributed by Jeff Hankins, 28-Jun-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (𝜃 → (𝜏 → (𝜑 → (𝜓 → (𝜒 → 𝜂)))))
Theorem	com5r 104	Commutation of antecedents. Rotate right. (Contributed by Wolf Lammen, 29-Jul-2012.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (𝜏 → (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜂)))))
Theorem	imim12 105	Closed form of imim12i 62 and of 3syl 18. (Contributed by BJ, 16-Jul-2019.)
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜃) → ((𝜓 → 𝜒) → (𝜑 → 𝜃))))
Theorem	jarr 106	Elimination of a nested antecedent. Sometimes called "Syll-Simp" since it is a syllogism applied to ax-1 6 ("Simplification"). (Contributed by Wolf Lammen, 9-May-2013.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒))
Theorem	jarri 107	Inference associated with jarr 106. Partial converse of ja 186 (the other partial converse being jarli 126). (Contributed by Wolf Lammen, 20-Sep-2013.)
⊢ ((𝜑 → 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	pm2.86d 108	Deduction associated with pm2.86 109. (Contributed by NM, 29-Jun-1995.) (Proof shortened by Wolf Lammen, 3-Apr-2013.)
⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	pm2.86 109	Converse of Axiom ax-2 7. Theorem *2.86 of [WhiteheadRussell] p. 108. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 3-Apr-2013.)
⊢ (((𝜑 → 𝜓) → (𝜑 → 𝜒)) → (𝜑 → (𝜓 → 𝜒)))
Theorem	pm2.86i 110	Inference associated with pm2.86 109. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Apr-2013.)
⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	loolin 111	The Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. See loowoz 112 for an alternate axiom. (Contributed by Mel L. O'Cat, 12-Aug-2004.)
⊢ (((𝜑 → 𝜓) → (𝜓 → 𝜑)) → (𝜓 → 𝜑))
Theorem	loowoz 112	An alternate for the Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz loolin 111, due to Barbara Wozniakowska, Reports on Mathematical Logic 10, 129-137 (1978). (Contributed by Mel L. O'Cat, 8-Aug-2004.)
⊢ (((𝜑 → 𝜓) → (𝜑 → 𝜒)) → ((𝜓 → 𝜑) → (𝜓 → 𝜒)))
1.2.4  Logical negation This section makes our first use of the third axiom of propositional calculus, ax-3 8. It introduces logical negation.
Theorem	con4 113	Alias for ax-3 8 to be used instead of it for labeling consistency. Its associated inference is con4i 114 and its associated deduction is con4d 115. (Contributed by BJ, 24-Dec-2020.)
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
Theorem	con4i 114	Inference associated with con4 113. Its associated inference is mt4 116. Remark: this can also be proved using notnot 142 followed by nsyl2 141, giving a shorter proof but depending on more axioms (namely, ax-1 6 and ax-2 7). (Contributed by NM, 29-Dec-1992.)
⊢ (¬ 𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜓 → 𝜑)
Theorem	con4d 115	Deduction associated with con4 113. (Contributed by NM, 26-Mar-1995.)
⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜓))
Theorem	mt4 116	The rule of modus tollens. Inference associated with con4i 114. (Contributed by Wolf Lammen, 12-May-2013.)
⊢ 𝜑    &   ⊢ (¬ 𝜓 → ¬ 𝜑)    ⇒   ⊢ 𝜓
Theorem	mt4d 117	Modus tollens deduction. Deduction form of mt4 116. (Contributed by NM, 9-Jun-2006.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	mt4i 118	Modus tollens inference. (Contributed by Wolf Lammen, 12-May-2013.)
⊢ 𝜒    &   ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.21i 119	A contradiction implies anything. Inference associated with pm2.21 123. Its associated inference is pm2.24ii 120. (Contributed by NM, 16-Sep-1993.)
⊢ ¬ 𝜑    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.24ii 120	A contradiction implies anything. Inference associated with pm2.21i 119 and pm2.24i 150. (Contributed by NM, 27-Feb-2008.)
⊢ 𝜑    &   ⊢ ¬ 𝜑    ⇒   ⊢ 𝜓
Theorem	pm2.21d 121	A contradiction implies anything. Deduction associated with pm2.21 123. (Contributed by NM, 10-Feb-1996.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	pm2.21ddALT 122	Alternate proof of pm2.21dd 194. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.21 123	From a wff and its negation, anything follows. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. Its commuted form is pm2.24 124 and its associated inference is pm2.21i 119. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 14-Sep-2012.)
⊢ (¬ 𝜑 → (𝜑 → 𝜓))
Theorem	pm2.24 124	Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 150. Commuted form of pm2.21 123. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 → (¬ 𝜑 → 𝜓))
Theorem	jarl 125	Elimination of a nested antecedent. (Contributed by Wolf Lammen, 10-May-2013.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (¬ 𝜑 → 𝜒))
Theorem	jarli 126	Inference associated with jarl 125. Partial converse of ja 186 (the other partial converse being jarri 107). (Contributed by Wolf Lammen, 4-Oct-2013.)
⊢ ((𝜑 → 𝜓) → 𝜒)    ⇒   ⊢ (¬ 𝜑 → 𝜒)
Theorem	pm2.18d 127	Deduction form of the Clavius law pm2.18 128. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.) Revised to shorten pm2.18 128. (Revised by Wolf Lammen, 17-Nov-2023.)
⊢ (𝜑 → (¬ 𝜓 → 𝜓))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.18 128	Clavius law, or "consequentia mirabilis" ("admirable consequence"). If a formula is implied by its negation, then it is true. Can be used in proofs by contradiction. Theorem *2.18 of [WhiteheadRussell] p. 103. See also the weak Clavius law pm2.01 188. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 17-Nov-2023.)
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
Theorem	pm2.18i 129	Inference associated with the Clavius law pm2.18 128. (Contributed by BJ, 30-Mar-2020.)
⊢ (¬ 𝜑 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	notnotr 130	Double negation elimination. Converse of notnot 142 and one implication of notnotb 315. Theorem *2.14 of [WhiteheadRussell] p. 102. This was the fifth axiom of Frege, specifically Proposition 31 of [Frege1879] p. 44. In classical logic (our logic) this is always true. In intuitionistic logic this is not always true, and formulas for which it is true are called "stable". (Contributed by NM, 29-Dec-1992.) (Proof shortened by David Harvey, 5-Sep-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
⊢ (¬ ¬ 𝜑 → 𝜑)
Theorem	notnotri 131	Inference associated with notnotr 130. For a shorter proof using ax-2 7, see notnotriALT 132. (Contributed by NM, 27-Feb-2008.) (Proof shortened by Wolf Lammen, 15-Jul-2021.) Remove dependency on ax-2 7. (Revised by Steven Nguyen, 27-Dec-2022.)
⊢ ¬ ¬ 𝜑    ⇒   ⊢ 𝜑
Theorem	notnotriALT 132	Alternate proof of notnotri 131. The proof via notnotr 130 and ax-mp 5 also has three essential steps, but has a total number of steps equal to 8, instead of the present 7, because it has to construct the formula 𝜑 twice and the formula ¬ ¬ 𝜑 once, whereas the present proof has to construct the formula 𝜑 twice and the formula ¬ 𝜑 once, and therefore makes only one use of wn 3 instead of two. This can be checked by running the Metamath command "MM> SHOW PROOF notnotri / NORMAL". (Contributed by NM, 27-Feb-2008.) (Proof shortened by Wolf Lammen, 15-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ¬ 𝜑    ⇒   ⊢ 𝜑
Theorem	notnotrd 133	Deduction associated with notnotr 130 and notnotri 131. Double negation elimination rule. A translation of the natural deduction rule ¬ ¬ C , Γ⊢ ¬ ¬ 𝜓 ⇒ Γ⊢ 𝜓; see natded 30165. This is Definition NNC in [Pfenning] p. 17. This rule is valid in classical logic (our logic), but not in intuitionistic logic. (Contributed by DAW, 8-Feb-2017.)
⊢ (𝜑 → ¬ ¬ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	con2d 134	A contraposition deduction. (Contributed by NM, 19-Aug-1993.)
⊢ (𝜑 → (𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 → ¬ 𝜓))
Theorem	con2 135	Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑))
Theorem	mt2d 136	Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → (𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	mt2i 137	Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
⊢ 𝜒    &   ⊢ (𝜑 → (𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	nsyl3 138	A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ (𝜒 → ¬ 𝜑)
Theorem	con2i 139	A contraposition inference. Its associated inference is mt2 199. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜓 → ¬ 𝜑)
Theorem	nsyl 140	A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	nsyl2 141	A negated syllogism inference. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 14-Nov-2023.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (¬ 𝜒 → 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	notnot 142	Double negation introduction. Converse of notnotr 130 and one implication of notnotb 315. Theorem *2.12 of [WhiteheadRussell] p. 101. This was the sixth axiom of Frege, specifically Proposition 41 of [Frege1879] p. 47. (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
⊢ (𝜑 → ¬ ¬ 𝜑)
Theorem	notnoti 143	Inference associated with notnot 142. (Contributed by NM, 27-Feb-2008.)
⊢ 𝜑    ⇒   ⊢ ¬ ¬ 𝜑
Theorem	notnotd 144	Deduction associated with notnot 142 and notnoti 143. (Contributed by Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf Lammen, 27-Mar-2021.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ¬ ¬ 𝜓)
Theorem	con1d 145	A contraposition deduction. (Contributed by NM, 27-Dec-1992.)
⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
Theorem	con1 146	Contraposition. Theorem *2.15 of [WhiteheadRussell] p. 102. Its associated inference is con1i 147. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
⊢ ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑))
Theorem	con1i 147	A contraposition inference. Inference associated with con1 146. Its associated inference is mt3 200. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 19-Jun-2013.)
⊢ (¬ 𝜑 → 𝜓)    ⇒   ⊢ (¬ 𝜓 → 𝜑)
Theorem	mt3d 148	Modus tollens deduction. (Contributed by NM, 26-Mar-1995.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	mt3i 149	Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
⊢ ¬ 𝜒    &   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.24i 150	Inference associated with pm2.24 124. Its associated inference is pm2.24ii 120. (Contributed by NM, 20-Aug-2001.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜑 → 𝜓)
Theorem	pm2.24d 151	Deduction form of pm2.24 124. (Contributed by NM, 30-Jan-2006.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
Theorem	con3d 152	A contraposition deduction. Deduction form of con3 153. (Contributed by NM, 10-Jan-1993.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
Theorem	con3 153	Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. This was the fourth axiom of Frege, specifically Proposition 28 of [Frege1879] p. 43. Its associated inference is con3i 154. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 13-Feb-2013.)
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))
Theorem	con3i 154	A contraposition inference. Inference associated with con3 153. Its associated inference is mto 196. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (¬ 𝜓 → ¬ 𝜑)
Theorem	con3rr3 155	Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (¬ 𝜒 → (𝜑 → ¬ 𝜓))
Theorem	nsyld 156	A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.)
⊢ (𝜑 → (𝜓 → ¬ 𝜒))    &   ⊢ (𝜑 → (𝜏 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ¬ 𝜏))
Theorem	nsyli 157	A negated syllogism inference. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → (𝜃 → ¬ 𝜓))
Theorem	nsyl4 158	A negated syllogism inference. (Contributed by NM, 15-Feb-1996.)
⊢ (𝜑 → 𝜓)    &   ⊢ (¬ 𝜑 → 𝜒)    ⇒   ⊢ (¬ 𝜒 → 𝜓)
Theorem	nsyl5 159	A negated syllogism inference. (Contributed by Wolf Lammen, 20-May-2024.)
⊢ (𝜑 → 𝜓)    &   ⊢ (¬ 𝜑 → 𝜒)    ⇒   ⊢ (¬ 𝜓 → 𝜒)
Theorem	pm3.2im 160	Theorem *3.2 of [WhiteheadRussell] p. 111, expressed with primitive connectives (see pm3.2 469). (Contributed by NM, 29-Dec-1992.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
Theorem	jc 161	Deduction joining the consequents of two premises. A deduction associated with pm3.2im 160. (Contributed by NM, 28-Dec-1992.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → ¬ (𝜓 → ¬ 𝜒))
Theorem	jcn 162	Theorem joining the consequents of two premises. Theorem 8 of [Margaris] p. 60. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
⊢ (𝜑 → (¬ 𝜓 → ¬ (𝜑 → 𝜓)))
Theorem	jcnd 163	Deduction joining the consequents of two premises. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Apr-2024.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → ¬ (𝜓 → 𝜒))
Theorem	impi 164	An importation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 20-Jul-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒)
Theorem	expi 165	An exportation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)
⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	simprim 166	Simplification. Similar to Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜓)
Theorem	simplim 167	Simplification. Similar to Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 21-Jul-2012.)
⊢ (¬ (𝜑 → 𝜓) → 𝜑)
Theorem	pm2.5g 168	General instance of Theorem *2.5 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 9-Oct-2012.)
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → 𝜒))
Theorem	pm2.5 169	Theorem *2.5 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → 𝜓))
Theorem	conax1 170	Contrapositive of ax-1 6. (Contributed by BJ, 28-Oct-2023.)
⊢ (¬ (𝜑 → 𝜓) → ¬ 𝜓)
Theorem	conax1k 171	Weakening of conax1 170. General instance of pm2.51 172 and of pm2.52 173. (Contributed by BJ, 28-Oct-2023.)
⊢ (¬ (𝜑 → 𝜓) → (𝜒 → ¬ 𝜓))
Theorem	pm2.51 172	Theorem *2.51 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 → 𝜓) → (𝜑 → ¬ 𝜓))
Theorem	pm2.52 173	Theorem *2.52 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.)
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → ¬ 𝜓))
Theorem	pm2.521g 174	A general instance of Theorem *2.521 of [WhiteheadRussell] p. 107. (Contributed by BJ, 28-Oct-2023.)
⊢ (¬ (𝜑 → 𝜓) → (𝜓 → 𝜒))
Theorem	pm2.521g2 175	A general instance of Theorem *2.521 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.)
⊢ (¬ (𝜑 → 𝜓) → (𝜒 → 𝜑))
Theorem	pm2.521 176	Theorem *2.521 of [WhiteheadRussell] p. 107. Instance of pm2.521g 174 and of pm2.521g2 175. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 → 𝜓) → (𝜓 → 𝜑))
Theorem	expt 177	Exportation theorem pm3.3 448 (closed form of ex 412) expressed with primitive connectives. (Contributed by NM, 28-Dec-1992.)
⊢ ((¬ (𝜑 → ¬ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
Theorem	impt 178	Importation theorem pm3.1 988 (closed form of imp 406) expressed with primitive connectives. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2013.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (¬ (𝜑 → ¬ 𝜓) → 𝜒))
Theorem	pm2.61d 179	Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.61d1 180	Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (¬ 𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.61d2 181	Inference eliminating an antecedent. (Contributed by NM, 18-Aug-1993.)
⊢ (𝜑 → (¬ 𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.61i 182	Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2023.)
⊢ (𝜑 → 𝜓)    &   ⊢ (¬ 𝜑 → 𝜓)    ⇒   ⊢ 𝜓
Theorem	pm2.61ii 183	Inference eliminating two antecedents. (Contributed by NM, 4-Jan-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ 𝜒
Theorem	pm2.61nii 184	Inference eliminating two antecedents. (Contributed by NM, 13-Jul-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (¬ 𝜑 → 𝜒)    &   ⊢ (¬ 𝜓 → 𝜒)    ⇒   ⊢ 𝜒
Theorem	pm2.61iii 185	Inference eliminating three antecedents. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
⊢ (¬ 𝜑 → (¬ 𝜓 → (¬ 𝜒 → 𝜃)))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ 𝜃
Theorem	ja 186	Inference joining the antecedents of two premises. For partial converses, see jarri 107 and jarli 126. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.)
⊢ (¬ 𝜑 → 𝜒)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ ((𝜑 → 𝜓) → 𝜒)
Theorem	jad 187	Deduction form of ja 186. (Contributed by Scott Fenton, 13-Dec-2010.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝜑 → (¬ 𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜒) → 𝜃))
Theorem	pm2.01 188	Weak Clavius law. If a formula implies its negation, then it is false. A form of "reductio ad absurdum", which can be used in proofs by contradiction. Theorem *2.01 of [WhiteheadRussell] p. 100. Provable in minimal calculus, contrary to the Clavius law pm2.18 128. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Mel L. O'Cat, 21-Nov-2008.) (Proof shortened by Wolf Lammen, 31-Oct-2012.)
⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑)
Theorem	pm2.01d 189	Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.)
⊢ (𝜑 → (𝜓 → ¬ 𝜓))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	pm2.6 190	Theorem *2.6 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜓) → 𝜓))
Theorem	pm2.61 191	Theorem *2.61 of [WhiteheadRussell] p. 107. Useful for eliminating an antecedent. (Contributed by NM, 4-Jan-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
⊢ ((𝜑 → 𝜓) → ((¬ 𝜑 → 𝜓) → 𝜓))
Theorem	pm2.65 192	Theorem *2.65 of [WhiteheadRussell] p. 107. Proof by contradiction. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 8-Mar-2013.)
⊢ ((𝜑 → 𝜓) → ((𝜑 → ¬ 𝜓) → ¬ 𝜑))
Theorem	pm2.65i 193	Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ ¬ 𝜑
Theorem	pm2.21dd 194	A contradiction implies anything. Deduction from pm2.21 123. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 22-Jul-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.65d 195	Deduction for proof by contradiction. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	mto 196	The rule of modus tollens. The rule says, "if 𝜓 is not true, and 𝜑 implies 𝜓, then 𝜑 must also be not true". Modus tollens is short for "modus tollendo tollens", a Latin phrase that means "the mode that by denying denies" - remark in [Sanford] p. 39. It is also called denying the consequent. Modus tollens is closely related to modus ponens ax-mp 5. Note that this rule is also valid in intuitionistic logic. Inference associated with con3i 154. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
⊢ ¬ 𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ ¬ 𝜑
Theorem	mtod 197	Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	mtoi 198	Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
⊢ ¬ 𝜒    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	mt2 199	A rule similar to modus tollens. Inference associated with con2i 139. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.)
⊢ 𝜓    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ ¬ 𝜑
Theorem	mt3 200	A rule similar to modus tollens. Inference associated with con1i 147. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
⊢ ¬ 𝜓    &   ⊢ (¬ 𝜑 → 𝜓)    ⇒   ⊢ 𝜑