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 175 (the other partial converse being jarli 124). (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 139 followed by nsyl2 145, 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	pm2.21i 117	A contradiction implies anything. Inference associated with pm2.21 121. Its associated inference is pm2.24ii 118. (Contributed by NM, 16-Sep-1993.)
⊢ ¬ 𝜑    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.24ii 118	A contradiction implies anything. Inference associated with pm2.21i 117 and pm2.24i 148. (Contributed by NM, 27-Feb-2008.)
⊢ 𝜑    &   ⊢ ¬ 𝜑    ⇒   ⊢ 𝜓
Theorem	pm2.21d 119	A contradiction implies anything. Deduction associated with pm2.21 121. (Contributed by NM, 10-Feb-1996.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	pm2.21ddALT 120	Alternate proof of pm2.21dd 187. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.21 121	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 122 and its associated inference is pm2.21i 117. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 14-Sep-2012.)
⊢ (¬ 𝜑 → (𝜑 → 𝜓))
Theorem	pm2.24 122	Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 148. Commuted form of pm2.21 121. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 → (¬ 𝜑 → 𝜓))
Theorem	jarl 123	Elimination of a nested antecedent. (Contributed by Wolf Lammen, 10-May-2013.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (¬ 𝜑 → 𝜒))
Theorem	jarli 124	Inference associated with jarl 123. Partial converse of ja 175 (the other partial converse being jarri 107). (Contributed by Wolf Lammen, 4-Oct-2013.)
⊢ ((𝜑 → 𝜓) → 𝜒)    ⇒   ⊢ (¬ 𝜑 → 𝜒)
Theorem	pm2.18 125	Clavius's 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 181. (Contributed by NM, 29-Dec-1992.)
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
Theorem	pm2.18i 126	Inference associated with the Clavius law pm2.18 125. (Contributed by BJ, 30-Mar-2020.)
⊢ (¬ 𝜑 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	pm2.18d 127	Deduction form of the Clavius law pm2.18 125. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → (¬ 𝜓 → 𝜓))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	notnotr 128	Double negation elimination. Converse of notnot 139 and one implication of notnotb 307. 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 129	Inference associated with notnotr 128. For a shorter proof using ax-2 7, see notnotriALT 130. (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 130	Alternate proof of notnotri 129. Inference associated with notnotr 128. Remark: the proof via notnotr 128 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 131	Deduction associated with notnotr 128 and notnotri 129. Double negation elimination rule. A translation of the natural deduction rule ¬ ¬ C , Γ⊢ ¬ ¬ 𝜓 ⇒ Γ⊢ 𝜓; see natded 27817. 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 132	A contraposition deduction. (Contributed by NM, 19-Aug-1993.)
⊢ (𝜑 → (𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 → ¬ 𝜓))
Theorem	con2 133	Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑))
Theorem	mt2d 134	Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → (𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	mt2i 135	Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
⊢ 𝜒    &   ⊢ (𝜑 → (𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	nsyl3 136	A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ (𝜒 → ¬ 𝜑)
Theorem	con2i 137	A contraposition inference. Its associated inference is mt2 192. (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 138	A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	notnot 139	Double negation introduction. Converse of notnotr 128 and one implication of notnotb 307. 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 140	Inference associated with notnot 139. (Contributed by NM, 27-Feb-2008.)
⊢ 𝜑    ⇒   ⊢ ¬ ¬ 𝜑
Theorem	notnotd 141	Deduction associated with notnot 139 and notnoti 140. (Contributed by Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf Lammen, 27-Mar-2021.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ¬ ¬ 𝜓)
Theorem	con1d 142	A contraposition deduction. (Contributed by NM, 27-Dec-1992.)
⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
Theorem	mt3d 143	Modus tollens deduction. (Contributed by NM, 26-Mar-1995.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	mt3i 144	Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
⊢ ¬ 𝜒    &   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	nsyl2 145	A negated syllogism inference. (Contributed by NM, 26-Jun-1994.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (¬ 𝜒 → 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
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 193. (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	pm2.24i 148	Inference associated with pm2.24 122. Its associated inference is pm2.24ii 118. (Contributed by NM, 20-Aug-2001.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜑 → 𝜓)
Theorem	pm2.24d 149	Deduction form of pm2.24 122. (Contributed by NM, 30-Jan-2006.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
Theorem	con3d 150	A contraposition deduction. Deduction form of con3 151. (Contributed by NM, 10-Jan-1993.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
Theorem	con3 151	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 152. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 13-Feb-2013.)
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))
Theorem	con3i 152	A contraposition inference. Inference associated with con3 151. Its associated inference is mto 189. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (¬ 𝜓 → ¬ 𝜑)
Theorem	con3rr3 153	Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (¬ 𝜒 → (𝜑 → ¬ 𝜓))
Theorem	mt4d 154	Modus tollens deduction. Deduction form of mt4 116. (Contributed by NM, 9-Jun-2006.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	mt4i 155	Modus tollens inference. (Contributed by Wolf Lammen, 12-May-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	pm3.2im 159	Theorem *3.2 of [WhiteheadRussell] p. 111, expressed with primitive connectives (see pm3.2 463). (Contributed by NM, 29-Dec-1992.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
Theorem	mth8 160	Theorem 8 of [Margaris] p. 60. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
⊢ (𝜑 → (¬ 𝜓 → ¬ (𝜑 → 𝜓)))
Theorem	jc 161	Deduction joining the consequents of two premises. A deduction associated with pm3.2im 159. (Contributed by NM, 28-Dec-1992.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → ¬ (𝜓 → ¬ 𝜒))
Theorem	impi 162	An importation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 20-Jul-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒)
Theorem	expi 163	An exportation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)
⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	simprim 164	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 165	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.5 166	Theorem *2.5 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 9-Oct-2012.)
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → 𝜓))
Theorem	pm2.51 167	Theorem *2.51 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 → 𝜓) → (𝜑 → ¬ 𝜓))
Theorem	pm2.521 168	Theorem *2.521 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.)
⊢ (¬ (𝜑 → 𝜓) → (𝜓 → 𝜑))
Theorem	pm2.52 169	Theorem *2.52 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.)
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → ¬ 𝜓))
Theorem	expt 170	Exportation theorem ex 403 expressed with primitive connectives. (Contributed by NM, 28-Dec-1992.)
⊢ ((¬ (𝜑 → ¬ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
Theorem	impt 171	Importation theorem imp 397 expressed with primitive connectives. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2013.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (¬ (𝜑 → ¬ 𝜓) → 𝜒))
Theorem	pm2.61d 172	Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.61d1 173	Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (¬ 𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.61d2 174	Inference eliminating an antecedent. (Contributed by NM, 18-Aug-1993.)
⊢ (𝜑 → (¬ 𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	ja 175	Inference joining the antecedents of two premises. For partial converses, see jarri 107 and jarli 124. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.)
⊢ (¬ 𝜑 → 𝜒)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ ((𝜑 → 𝜓) → 𝜒)
Theorem	jad 176	Deduction form of ja 175. (Contributed by Scott Fenton, 13-Dec-2010.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝜑 → (¬ 𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜒) → 𝜃))
Theorem	pm2.61i 177	Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)
⊢ (𝜑 → 𝜓)    &   ⊢ (¬ 𝜑 → 𝜓)    ⇒   ⊢ 𝜓
Theorem	pm2.61ii 178	Inference eliminating two antecedents. (Contributed by NM, 4-Jan-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ 𝜒
Theorem	pm2.61nii 179	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 180	Inference eliminating three antecedents. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
⊢ (¬ 𝜑 → (¬ 𝜓 → (¬ 𝜒 → 𝜃)))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ 𝜃
Theorem	pm2.01 181	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 125. (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 182	Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.)
⊢ (𝜑 → (𝜓 → ¬ 𝜓))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	pm2.6 183	Theorem *2.6 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜓) → 𝜓))
Theorem	pm2.61 184	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 185	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 186	Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ ¬ 𝜑
Theorem	pm2.21dd 187	A contradiction implies anything. Deduction from pm2.21 121. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 22-Jul-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.65d 188	Deduction for proof by contradiction. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	mto 189	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 152. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
⊢ ¬ 𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ ¬ 𝜑
Theorem	mtod 190	Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	mtoi 191	Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
⊢ ¬ 𝜒    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	mt2 192	A rule similar to modus tollens. Inference associated with con2i 137. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.)
⊢ 𝜓    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ ¬ 𝜑
Theorem	mt3 193	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.)
⊢ ¬ 𝜓    &   ⊢ (¬ 𝜑 → 𝜓)    ⇒   ⊢ 𝜑
Theorem	peirce 194	Peirce's axiom. A non-intuitionistic implication-only statement. Added to intuitionistic (implicational) propositional calculus, it gives classical (implicational) propositional calculus. For another non-intuitionistic positive statement, see curryax 924. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 9-Oct-2012.)
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
Theorem	looinv 195	The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. Using dfor2 932, we can see that this essentially expresses "disjunction commutes". Theorem *2.69 of [WhiteheadRussell] p. 108. It is a special instance of the axiom "Roll", see peirceroll 85. (Contributed by NM, 12-Aug-2004.)
⊢ (((𝜑 → 𝜓) → 𝜓) → ((𝜓 → 𝜑) → 𝜑))
Theorem	bijust0 196	A self-implication (see id 22) does not imply its own negation. The justification theorem bijust 197 is one of its instances. (Contributed by NM, 11-May-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.) Extract bijust0 196 from proof of bijust 197. (Revised by BJ, 19-Mar-2020.)
⊢ ¬ ((𝜑 → 𝜑) → ¬ (𝜑 → 𝜑))
Theorem	bijust 197	Theorem used to justify the definition of the biconditional df-bi 199. Instance of bijust0 196. (Contributed by NM, 11-May-1999.)
⊢ ¬ ((¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))))
1.2.5  Logical equivalence The definition df-bi 199 in this section is our first definition, which introduces and defines the biconditional connective ↔ used to denote logical equivalence. We define a wff of the form (𝜑 ↔ 𝜓) as an abbreviation for ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)). 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 (df-or 881 is its first use), as it allows us to use logic to manipulate definitions directly. This greatly simplifies many proofs since it eliminates the need for a separate mechanism for introducing and eliminating definitions. A note on definitions: definitions are required to be eliminable (that is, a theorem stated in terms of the defined symbol can also be stated without it) and conservative (that is, a theorem whose statement does not contain the defined symbol can be proved without using that definition). This means that a definition does not increase the expressive power nor the deductive power, respectively, of a theory. On the other hand, definitions are often useful to write shorter proofs, so in (i)set.mm we will generally not try to avoid them. This is why, for instance, some theorems which do not contain disjunction in their statement are placed after the section on disjunction because a shorter proof using disjunction is possible.
Syntax	wb 198	Extend wff definition to include the biconditional connective.
wff (𝜑 ↔ 𝜓)
Definition	df-bi 199	Define the biconditional (logical "iff" or "if and only if"). The definition df-bi 199 in this section is our first definition, which introduces and defines the biconditional connective ↔. We define a wff of the form (𝜑 ↔ 𝜓) as an abbreviation for ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)). 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 (df-or 881 is its first use), as it allows us to use logic to manipulate definitions directly. This greatly simplifies many proofs since it eliminates the need for a separate mechanism for introducing and eliminating definitions. Of course, we cannot use this mechanism to define the biconditional itself, since it hasn't been introduced yet. Instead, we use a more general form of definition, described as follows. In its most general form, a definition is simply an assertion that introduces a new symbol (or a new combination of existing symbols, as in df-3an 1115) that is eliminable and does not strengthen the existing language. The latter requirement means that the set of provable statements not containing the new symbol (or new combination) should remain exactly the same after the definition is introduced. Our definition of the biconditional may look unusual compared to most definitions, but it strictly satisfies these requirements. The justification for our definition is that if we mechanically replace (𝜑 ↔ 𝜓) (the definiendum i.e. the thing being defined) with ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) (the definiens i.e. the defining expression) in the definition, the definition becomes the previously proved theorem bijust 197. It is impossible to use df-bi 199 to prove any statement expressed in the original language that can't be proved from the original axioms, because if we simply replace each instance of df-bi 199 in the proof with the corresponding bijust 197 instance, we will end up with a proof from the original axioms. Note that from Metamath's point of view, a definition is just another axiom - i.e. an assertion we claim to be true - but from our high level point of view, we are not strengthening the language. 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 a naming convention for human readability.) After we define the constant true ⊤ (df-tru 1662) and the constant false ⊥ (df-fal 1672), we will be able to prove these truth table values: ((⊤ ↔ ⊤) ↔ ⊤) (trubitru 1688), ((⊤ ↔ ⊥) ↔ ⊥) (trubifal 1690), ((⊥ ↔ ⊤) ↔ ⊥) (falbitru 1689), and ((⊥ ↔ ⊥) ↔ ⊤) (falbifal 1691). See dfbi1 205, dfbi2 468, and dfbi3 1078 for theorems suggesting typical textbook definitions of ↔, showing that our definition has the properties we expect. Theorem dfbi1 205 is particularly useful if we want to eliminate ↔ from an expression to convert it to primitives. Theorem dfbi 469 shows this definition rewritten in an abbreviated form after conjunction is introduced, for easier understanding. Contrast with ∨ (df-or 881), → (wi 4), ⊼ (df-nan 1615), and ⊻ (df-xor 1640). In some sense ↔ returns true if two truth values are equal; = (df-cleq 2817) returns true if two classes are equal. (Contributed by NM, 27-Dec-1992.)
⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
Theorem	impbi 200	Property of the biconditional connective. (Contributed by NM, 11-May-1999.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → (𝜑 ↔ 𝜓)))