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 189 (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 144 followed by nsyl2 143, 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 153. (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 198. (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 153. 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 189 (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 192. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 17-Nov-2023.)
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
Theorem	pm2.18OLD 129	Obsolete version of pm2.18 128 as of 17-Nov-2023. (Contributed by NM, 29-Dec-1992.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
Theorem	pm2.18dOLD 130	Obsolete version of pm2.18d 127 as of 17-Nov-2023. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (¬ 𝜓 → 𝜓))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.18i 131	Inference associated with the Clavius law pm2.18 128. (Contributed by BJ, 30-Mar-2020.)
⊢ (¬ 𝜑 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	notnotr 132	Double negation elimination. Converse of notnot 144 and one implication of notnotb 318. 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 133	Inference associated with notnotr 132. For a shorter proof using ax-2 7, see notnotriALT 134. (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 134	Alternate proof of notnotri 133. The proof via notnotr 132 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 135	Deduction associated with notnotr 132 and notnotri 133. Double negation elimination rule. A translation of the natural deduction rule ¬ ¬ C , Γ⊢ ¬ ¬ 𝜓 ⇒ Γ⊢ 𝜓; see natded 28302. 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 136	A contraposition deduction. (Contributed by NM, 19-Aug-1993.)
⊢ (𝜑 → (𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 → ¬ 𝜓))
Theorem	con2 137	Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑))
Theorem	mt2d 138	Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → (𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	mt2i 139	Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
⊢ 𝜒    &   ⊢ (𝜑 → (𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	nsyl3 140	A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ (𝜒 → ¬ 𝜑)
Theorem	con2i 141	A contraposition inference. Its associated inference is mt2 203. (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 142	A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	nsyl2 143	A negated syllogism inference. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 14-Nov-2023.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (¬ 𝜒 → 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	notnot 144	Double negation introduction. Converse of notnotr 132 and one implication of notnotb 318. 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 145	Inference associated with notnot 144. (Contributed by NM, 27-Feb-2008.)
⊢ 𝜑    ⇒   ⊢ ¬ ¬ 𝜑
Theorem	notnotd 146	Deduction associated with notnot 144 and notnoti 145. (Contributed by Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf Lammen, 27-Mar-2021.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ¬ ¬ 𝜓)
Theorem	con1d 147	A contraposition deduction. (Contributed by NM, 27-Dec-1992.)
⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
Theorem	con1 148	Contraposition. Theorem *2.15 of [WhiteheadRussell] p. 102. Its associated inference is con1i 149. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
⊢ ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑))
Theorem	con1i 149	A contraposition inference. Inference associated with con1 148. Its associated inference is mt3 204. (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 150	Modus tollens deduction. (Contributed by NM, 26-Mar-1995.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	mt3i 151	Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
⊢ ¬ 𝜒    &   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	nsyl2OLD 152	Obsolete version of nsyl2 143 as of 14-Nov-2023. (Contributed by NM, 26-Jun-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (¬ 𝜒 → 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.24i 153	Inference associated with pm2.24 124. Its associated inference is pm2.24ii 120. (Contributed by NM, 20-Aug-2001.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜑 → 𝜓)
Theorem	pm2.24d 154	Deduction form of pm2.24 124. (Contributed by NM, 30-Jan-2006.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
Theorem	con3d 155	A contraposition deduction. Deduction form of con3 156. (Contributed by NM, 10-Jan-1993.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
Theorem	con3 156	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 157. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 13-Feb-2013.)
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))
Theorem	con3i 157	A contraposition inference. Inference associated with con3 156. Its associated inference is mto 200. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (¬ 𝜓 → ¬ 𝜑)
Theorem	con3rr3 158	Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (¬ 𝜒 → (𝜑 → ¬ 𝜓))
Theorem	nsyld 159	A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.)
⊢ (𝜑 → (𝜓 → ¬ 𝜒))    &   ⊢ (𝜑 → (𝜏 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ¬ 𝜏))
Theorem	nsyli 160	A negated syllogism inference. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → (𝜃 → ¬ 𝜓))
Theorem	nsyl4 161	A negated syllogism inference. (Contributed by NM, 15-Feb-1996.)
⊢ (𝜑 → 𝜓)    &   ⊢ (¬ 𝜑 → 𝜒)    ⇒   ⊢ (¬ 𝜒 → 𝜓)
Theorem	nsyl5 162	A negated syllogism inference. (Contributed by Wolf Lammen, 20-May-2024.)
⊢ (𝜑 → 𝜓)    &   ⊢ (¬ 𝜑 → 𝜒)    ⇒   ⊢ (¬ 𝜓 → 𝜒)
Theorem	pm3.2im 163	Theorem *3.2 of [WhiteheadRussell] p. 111, expressed with primitive connectives (see pm3.2 473). (Contributed by NM, 29-Dec-1992.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
Theorem	jc 164	Deduction joining the consequents of two premises. A deduction associated with pm3.2im 163. (Contributed by NM, 28-Dec-1992.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → ¬ (𝜓 → ¬ 𝜒))
Theorem	jcn 165	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 166	Deduction joining the consequents of two premises. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Apr-2024.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → ¬ (𝜓 → 𝜒))
Theorem	impi 167	An importation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 20-Jul-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒)
Theorem	expi 168	An exportation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)
⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	simprim 169	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 170	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 171	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 172	Theorem *2.5 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → 𝜓))
Theorem	conax1 173	Contrapositive of ax-1 6. (Contributed by BJ, 28-Oct-2023.)
⊢ (¬ (𝜑 → 𝜓) → ¬ 𝜓)
Theorem	conax1k 174	Weakening of conax1 173. General instance of pm2.51 175 and of pm2.52 176. (Contributed by BJ, 28-Oct-2023.)
⊢ (¬ (𝜑 → 𝜓) → (𝜒 → ¬ 𝜓))
Theorem	pm2.51 175	Theorem *2.51 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 → 𝜓) → (𝜑 → ¬ 𝜓))
Theorem	pm2.52 176	Theorem *2.52 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.)
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → ¬ 𝜓))
Theorem	pm2.521g 177	A general instance of Theorem *2.521 of [WhiteheadRussell] p. 107. (Contributed by BJ, 28-Oct-2023.)
⊢ (¬ (𝜑 → 𝜓) → (𝜓 → 𝜒))
Theorem	pm2.521g2 178	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 179	Theorem *2.521 of [WhiteheadRussell] p. 107. Instance of pm2.521g 177 and of pm2.521g2 178. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 → 𝜓) → (𝜓 → 𝜑))
Theorem	expt 180	Exportation theorem pm3.3 452 (closed form of ex 416) expressed with primitive connectives. (Contributed by NM, 28-Dec-1992.)
⊢ ((¬ (𝜑 → ¬ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
Theorem	impt 181	Importation theorem pm3.1 989 (closed form of imp 410) expressed with primitive connectives. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2013.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (¬ (𝜑 → ¬ 𝜓) → 𝜒))
Theorem	pm2.61d 182	Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.61d1 183	Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (¬ 𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.61d2 184	Inference eliminating an antecedent. (Contributed by NM, 18-Aug-1993.)
⊢ (𝜑 → (¬ 𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.61i 185	Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2023.)
⊢ (𝜑 → 𝜓)    &   ⊢ (¬ 𝜑 → 𝜓)    ⇒   ⊢ 𝜓
Theorem	pm2.61ii 186	Inference eliminating two antecedents. (Contributed by NM, 4-Jan-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ 𝜒
Theorem	pm2.61nii 187	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 188	Inference eliminating three antecedents. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
⊢ (¬ 𝜑 → (¬ 𝜓 → (¬ 𝜒 → 𝜃)))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ 𝜃
Theorem	ja 189	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 190	Deduction form of ja 189. (Contributed by Scott Fenton, 13-Dec-2010.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝜑 → (¬ 𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜒) → 𝜃))
Theorem	pm2.61iOLD 191	Obsolete version of pm2.61i 185 as of 19-Nov-2023. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (¬ 𝜑 → 𝜓)    ⇒   ⊢ 𝜓
Theorem	pm2.01 192	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 193	Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.)
⊢ (𝜑 → (𝜓 → ¬ 𝜓))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	pm2.6 194	Theorem *2.6 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜓) → 𝜓))
Theorem	pm2.61 195	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 196	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 197	Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ ¬ 𝜑
Theorem	pm2.21dd 198	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 199	Deduction for proof by contradiction. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	mto 200	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 157. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
⊢ ¬ 𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ ¬ 𝜑