P. 4 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 301-400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	3bitr3d 301	Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜃 ↔ 𝜏))
Theorem	3bitr3rd 302	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜏 ↔ 𝜃))
Theorem	3bitr4d 303	Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜓))    &   ⊢ (𝜑 → (𝜏 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜃 ↔ 𝜏))
Theorem	3bitr4rd 304	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜓))    &   ⊢ (𝜑 → (𝜏 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜏 ↔ 𝜃))
Theorem	3bitr3g 305	More general version of 3bitr3i 293. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜓 ↔ 𝜃)    &   ⊢ (𝜒 ↔ 𝜏)    ⇒   ⊢ (𝜑 → (𝜃 ↔ 𝜏))
Theorem	3bitr4g 306	More general version of 3bitr4i 295. Useful for converting definitions in a formula. (Contributed by NM, 11-May-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜒)    ⇒   ⊢ (𝜑 → (𝜃 ↔ 𝜏))
Theorem	notnotb 307	Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 ↔ ¬ ¬ 𝜑)
Theorem	con34b 308	A biconditional form of contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116. (Contributed by NM, 11-May-1993.)
⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
Theorem	con4bid 309	A contraposition deduction. (Contributed by NM, 21-May-1994.)
⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	notbid 310	Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
Theorem	notbi 311	Contraposition. Theorem *4.11 of [WhiteheadRussell] p. 117. (Contributed by NM, 21-May-1994.) (Proof shortened by Wolf Lammen, 12-Jun-2013.)
⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
Theorem	notbii 312	Negate both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (¬ 𝜑 ↔ ¬ 𝜓)
Theorem	con4bii 313	A contraposition inference. (Contributed by NM, 21-May-1994.)
⊢ (¬ 𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	mtbi 314	An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
⊢ ¬ 𝜑    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ¬ 𝜓
Theorem	mtbir 315	An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.)
⊢ ¬ 𝜓    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ¬ 𝜑
Theorem	mtbid 316	A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	mtbird 317	A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	mtbii 318	An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.)
⊢ ¬ 𝜓    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	mtbiri 319	An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.)
⊢ ¬ 𝜒    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	sylnib 320	A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	sylnibr 321	A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	sylnbi 322	A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (¬ 𝜓 → 𝜒)    ⇒   ⊢ (¬ 𝜑 → 𝜒)
Theorem	sylnbir 323	A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ (¬ 𝜓 → 𝜒)    ⇒   ⊢ (¬ 𝜑 → 𝜒)
Theorem	xchnxbi 324	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
⊢ (¬ 𝜑 ↔ 𝜓)    &   ⊢ (𝜑 ↔ 𝜒)    ⇒   ⊢ (¬ 𝜒 ↔ 𝜓)
Theorem	xchnxbir 325	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
⊢ (¬ 𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜑)    ⇒   ⊢ (¬ 𝜒 ↔ 𝜓)
Theorem	xchbinx 326	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
⊢ (𝜑 ↔ ¬ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (𝜑 ↔ ¬ 𝜒)
Theorem	xchbinxr 327	Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
⊢ (𝜑 ↔ ¬ 𝜓)    &   ⊢ (𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ ¬ 𝜒)
Theorem	imbi2i 328	Introduce an antecedent to both sides of a logical equivalence. This and the next three rules are useful for building up wff's around a definition, in order to make use of the definition. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))
Theorem	jcn 329	Inference joining the consequents of two premises. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → ¬ (𝜓 → 𝜒))
Theorem	bibi2i 330	Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))
Theorem	bibi1i 331	Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 26-May-1993.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))
Theorem	bibi12i 332	The equivalence of two equivalences. (Contributed by NM, 26-May-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜃))
Theorem	imbi2d 333	Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒)))
Theorem	imbi1d 334	Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))
Theorem	bibi2d 335	Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))
Theorem	bibi1d 336	Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 11-May-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))
Theorem	imbi12d 337	Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 16-May-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))
Theorem	bibi12d 338	Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 26-May-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))
Theorem	imbi12 339	Closed form of imbi12i 343. Was automatically derived from its "Virtual Deduction" version and the Metamath program "MM-PA> MINIMIZE_WITH *" command. (Contributed by Alan Sare, 18-Mar-2012.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))))
Theorem	imbi1 340	Theorem *4.84 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
Theorem	imbi2 341	Theorem *4.85 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)))
Theorem	imbi1i 342	Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))
Theorem	imbi12i 343	Join two logical equivalences to form equivalence of implications. (Contributed by NM, 1-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))
Theorem	bibi1 344	Theorem *4.86 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒)))
Theorem	bitr3 345	Closed nested implication form of bitr3i 269. Derived automatically from bitr3VD 40602. (Contributed by Alan Sare, 31-Dec-2011.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) → (𝜓 ↔ 𝜒)))
Theorem	con2bi 346	Contraposition. Theorem *4.12 of [WhiteheadRussell] p. 117. (Contributed by NM, 15-Apr-1995.) (Proof shortened by Wolf Lammen, 3-Jan-2013.)
⊢ ((𝜑 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜑))
Theorem	con2bid 347	A contraposition deduction. (Contributed by NM, 15-Apr-1995.)
⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))
Theorem	con1bid 348	A contraposition deduction. (Contributed by NM, 9-Oct-1999.)
⊢ (𝜑 → (¬ 𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (¬ 𝜒 ↔ 𝜓))
Theorem	con1bii 349	A contraposition inference. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)
⊢ (¬ 𝜑 ↔ 𝜓)    ⇒   ⊢ (¬ 𝜓 ↔ 𝜑)
Theorem	con2bii 350	A contraposition inference. (Contributed by NM, 12-Mar-1993.)
⊢ (𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (𝜓 ↔ ¬ 𝜑)
Theorem	con1b 351	Contraposition. Bidirectional version of con1 146. (Contributed by NM, 3-Jan-1993.)
⊢ ((¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → 𝜑))
Theorem	con2b 352	Contraposition. Bidirectional version of con2 133. (Contributed by NM, 12-Mar-1993.)
⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑))
Theorem	biimt 353	A wff is equivalent to itself with true antecedent. (Contributed by NM, 28-Jan-1996.)
⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))
Theorem	pm5.5 354	Theorem *5.5 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓))
Theorem	a1bi 355	Inference introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜑 → 𝜓))
Theorem	mt2bi 356	A false consequent falsifies an antecedent. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜓 ↔ (𝜓 → ¬ 𝜑))
Theorem	mtt 357	Modus-tollens-like theorem. (Contributed by NM, 7-Apr-2001.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)
⊢ (¬ 𝜑 → (¬ 𝜓 ↔ (𝜓 → 𝜑)))
Theorem	imnot 358	If a proposition is false, then implying it is equivalent to being false. One of four theorems that can be used to simplify an implication (𝜑 → 𝜓), the other ones being ax-1 6 (true consequent), pm2.21 121 (false antecedent), pm5.5 354 (true antecedent). (Contributed by Mario Carneiro, 26-Apr-2019.) (Proof shortened by Wolf Lammen, 26-May-2019.)
⊢ (¬ 𝜓 → ((𝜑 → 𝜓) ↔ ¬ 𝜑))
Theorem	pm5.501 359	Theorem *5.501 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 → (𝜓 ↔ (𝜑 ↔ 𝜓)))
Theorem	ibib 360	Implication in terms of implication and biconditional. (Contributed by NM, 31-Mar-1994.) (Proof shortened by Wolf Lammen, 24-Jan-2013.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜑 ↔ 𝜓)))
Theorem	ibibr 361	Implication in terms of implication and biconditional. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 21-Dec-2013.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜓 ↔ 𝜑)))
Theorem	tbt 362	A wff is equivalent to its equivalence with a truth. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜓 ↔ 𝜑))
Theorem	nbn2 363	The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by Juha Arpiainen, 19-Jan-2006.) (Proof shortened by Wolf Lammen, 28-Jan-2013.)
⊢ (¬ 𝜑 → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓)))
Theorem	bibif 364	Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007.) (Proof shortened by Wolf Lammen, 28-Jan-2013.)
⊢ (¬ 𝜓 → ((𝜑 ↔ 𝜓) ↔ ¬ 𝜑))
Theorem	nbn 365	The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ ¬ 𝜑    ⇒   ⊢ (¬ 𝜓 ↔ (𝜓 ↔ 𝜑))
Theorem	nbn3 366	Transfer falsehood via equivalence. (Contributed by NM, 11-Sep-2006.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜓 ↔ (𝜓 ↔ ¬ 𝜑))
Theorem	pm5.21im 367	Two propositions are equivalent if they are both false. Closed form of 2false 368. Equivalent to a biimpr 212-like version of the xor-connective. (Contributed by Wolf Lammen, 13-May-2013.)
⊢ (¬ 𝜑 → (¬ 𝜓 → (𝜑 ↔ 𝜓)))
Theorem	2false 368	Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.)
⊢ ¬ 𝜑    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	2falsed 369	Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	pm5.21ni 370	Two propositions implying a false one are equivalent. (Contributed by NM, 16-Feb-1996.) (Proof shortened by Wolf Lammen, 19-May-2013.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒))
Theorem	pm5.21nii 371	Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜓)    &   ⊢ (𝜓 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (𝜑 ↔ 𝜒)
Theorem	pm5.21ndd 372	Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Proof shortened by Wolf Lammen, 6-Oct-2013.)
⊢ (𝜑 → (𝜒 → 𝜓))    &   ⊢ (𝜑 → (𝜃 → 𝜓))    &   ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜒 ↔ 𝜃))
Theorem	bija 373	Combine antecedents into a single biconditional. This inference, reminiscent of ja 175, is reversible: The hypotheses can be deduced from the conclusion alone (see pm5.1im 255 and pm5.21im 367). (Contributed by Wolf Lammen, 13-May-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ↔ 𝜓) → 𝜒)
Theorem	pm5.18 374	Theorem *5.18 of [WhiteheadRussell] p. 124. This theorem says that logical equivalence is the same as negated "exclusive or". (Contributed by NM, 28-Jun-2002.) (Proof shortened by Andrew Salmon, 20-Jun-2011.) (Proof shortened by Wolf Lammen, 15-Oct-2013.)
⊢ ((𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ↔ ¬ 𝜓))
Theorem	xor3 375	Two ways to express "exclusive or". (Contributed by NM, 1-Jan-2006.)
⊢ (¬ (𝜑 ↔ 𝜓) ↔ (𝜑 ↔ ¬ 𝜓))
Theorem	nbbn 376	Move negation outside of biconditional. Compare Theorem *5.18 of [WhiteheadRussell] p. 124. (Contributed by NM, 27-Jun-2002.) (Proof shortened by Wolf Lammen, 20-Sep-2013.)
⊢ ((¬ 𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))
Theorem	biass 377	Associative law for the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs", Annals of Pure and Applied Logic, 113:207-224, 2002, http://www.cs.utexas.edu/users/ai-lab/pub-view.php?PubID=26805. Interestingly, this law was not included in Principia Mathematica but was apparently first noted by Jan Lukasiewicz circa 1923. (Contributed by NM, 8-Jan-2005.) (Proof shortened by Juha Arpiainen, 19-Jan-2006.) (Proof shortened by Wolf Lammen, 21-Sep-2013.)
⊢ (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒)))
Theorem	biluk 378	Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall, ed., Polish Logic 1920-1939 (Oxford, 1967), p. 96. (Contributed by NM, 10-Jan-2005.)
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒)))
Theorem	pm5.19 379	Theorem *5.19 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.)
⊢ ¬ (𝜑 ↔ ¬ 𝜑)
Theorem	bi2.04 380	Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 11-May-1993.)
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))
Theorem	pm5.4 381	Antecedent absorption implication. Theorem *5.4 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.)
⊢ ((𝜑 → (𝜑 → 𝜓)) ↔ (𝜑 → 𝜓))
Theorem	imdi 382	Distributive law for implication. Compare Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.)
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	pm5.41 383	Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 12-Oct-2012.)
⊢ (((𝜑 → 𝜓) → (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 → 𝜒)))
Theorem	pm4.8 384	Theorem *4.8 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → ¬ 𝜑) ↔ ¬ 𝜑)
Theorem	pm4.81 385	A formula is equivalent to its negation implying it. Theorem *4.81 of [WhiteheadRussell] p. 122. Note that the second step, using pm2.24 122, could also use ax-1 6. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 → 𝜑) ↔ 𝜑)
Theorem	imim21b 386	Simplify an implication between two implications when the antecedent of the first is a consequence of the antecedent of the second. The reverse form is useful in producing the successor step in induction proofs. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Wolf Lammen, 14-Sep-2013.)
⊢ ((𝜓 → 𝜑) → (((𝜑 → 𝜒) → (𝜓 → 𝜃)) ↔ (𝜓 → (𝜒 → 𝜃))))
1.2.6  Logical conjunction This section defines conjunction of two formulas, denoted by infix "∧ " and read "and". It is defined in terms of implication and negation, which is possible in classical logic (but not in intuitionistic logic: see iset.mm). After the definition, we briefly introduce conversion of simple expressions to and from conjunction. Two simple operations called importation (imp 398) and exportation (ex 405) follow. In the propositions-as-types interpretation, they correspond to uncurrying and currying respectively. They are foundational for this section. Most of the theorems proved here trace back to them, mostly indirectly, in a layered fashion, where more complex expressions are built from simpler ones. Here are some of these successive layers: importation and exportation, commutativity and associativity laws, adding antecedents and simplifying, conjunction of consequents, syllogisms, etc. As indicated in the "note on definitions" in the section comment for logical equivalence, some theorems containing only implication, negation and conjunction are placed in the section after disjunction since theirs proofs use disjunction (although this is not required since definitions are conservative, see said section comment).
Syntax	wa 387	Extend wff definition to include conjunction ("and").
wff (𝜑 ∧ 𝜓)
Definition	df-an 388	Define conjunction (logical "and"). Definition of [Margaris] p. 49. When both the left and right operand are true, the result is true; when either is false, the result is false. For example, it is true that (2 = 2 ∧ 3 = 3). After we define the constant true ⊤ (df-tru 1510) and the constant false ⊥ (df-fal 1520), we will be able to prove these truth table values: ((⊤ ∧ ⊤) ↔ ⊤) (truantru 1540), ((⊤ ∧ ⊥) ↔ ⊥) (truanfal 1541), ((⊥ ∧ ⊤) ↔ ⊥) (falantru 1542), and ((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1543). This is our first use of the biconditional connective in a definition; we use the biconditional connective in place of the traditional "<=def=>", which means the same thing, except that we can manipulate the biconditional connective directly in proofs rather than having to rely on an informal definition substitution rule. Note that if we mechanically substitute ¬ (𝜑 → ¬ 𝜓) for (𝜑 ∧ 𝜓), we end up with an instance of previously proved theorem biid 253. This is the justification for the definition, along with the fact that it introduces a new symbol ∧. Contrast with ∨ (df-or 834), → (wi 4), ⊼ (df-nan 1464), and ⊻ (df-xor 1489). (Contributed by NM, 5-Jan-1993.)
⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
Theorem	pm4.63 389	Theorem *4.63 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 → ¬ 𝜓) ↔ (𝜑 ∧ 𝜓))
Theorem	pm4.67 390	Theorem *4.67 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∧ 𝜓))
Theorem	imnan 391	Express an implication in terms of a negated conjunction. (Contributed by NM, 9-Apr-1994.)
⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
Theorem	imnani 392	Infer an implication from a negated conjunction. (Contributed by Mario Carneiro, 28-Sep-2015.)
⊢ ¬ (𝜑 ∧ 𝜓)    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	iman 393	Implication in terms of conjunction and negation. Theorem 3.4(27) of [Stoll] p. 176. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2012.)
⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
Theorem	pm3.24 394	Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who call it the "law of contradiction"). (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ¬ (𝜑 ∧ ¬ 𝜑)
Theorem	annim 395	Express a conjunction in terms of a negated implication. (Contributed by NM, 2-Aug-1994.)
⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))
Theorem	pm4.61 396	Theorem *4.61 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 → 𝜓) ↔ (𝜑 ∧ ¬ 𝜓))
Theorem	pm4.65 397	Theorem *4.65 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 → 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
Theorem	imp 398	Importation inference. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	impcom 399	Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
Theorem	con3dimp 400	Variant of con3d 150 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)