P. 16 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 1501-1600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	3anandirs 1501	Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 25-Jul-2006.)
⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	ecase13d 1502	Deduction for elimination by cases. (Contributed by Jeff Hankins, 18-Aug-2009.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	ecase23d 1503	Deduction for elimination by cases. (Contributed by NM, 22-Apr-1994.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	ecase33d 1504	Deduction for elimination by cases. (Contributed by Thierry Arnoux, 5-Jul-2026.)
⊢ (𝜑 → ¬ 𝜓)    &   ⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	3ecase 1505	Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.)
⊢ (¬ 𝜑 → 𝜃)    &   ⊢ (¬ 𝜓 → 𝜃)    &   ⊢ (¬ 𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	3bior1fd 1506	A disjunction is equivalent to a threefold disjunction with single falsehood, analogous to biorf 949. (Contributed by Alexander van der Vekens, 8-Sep-2017.)
⊢ (𝜑 → ¬ 𝜃)    ⇒   ⊢ (𝜑 → ((𝜒 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒 ∨ 𝜓)))
Theorem	3bior1fand 1507	A disjunction is equivalent to a threefold disjunction with single falsehood of a conjunction. (Contributed by Alexander van der Vekens, 8-Sep-2017.)
⊢ (𝜑 → ¬ 𝜃)    ⇒   ⊢ (𝜑 → ((𝜒 ∨ 𝜓) ↔ ((𝜃 ∧ 𝜏) ∨ 𝜒 ∨ 𝜓)))
Theorem	3bior2fd 1508	A wff is equivalent to its threefold disjunction with double falsehood, analogous to biorf 949. (Contributed by Alexander van der Vekens, 8-Sep-2017.)
⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜃 ∨ 𝜒 ∨ 𝜓)))
Theorem	3biant1d 1509	A conjunction is equivalent to a threefold conjunction with single truth, analogous to biantrud 540. (Contributed by Alexander van der Vekens, 26-Sep-2017.)
⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒 ∧ 𝜓)))
Theorem	intn3an1d 1510	Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	intn3an2d 1511	Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓 ∧ 𝜃))
Theorem	intn3an3d 1512	Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜃 ∧ 𝜓))
Theorem	an3andi 1513	Distribution of conjunction over threefold conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒) ∧ (𝜑 ∧ 𝜃)))
Theorem	an33rean 1514	Rearrange a 9-fold conjunction. (Contributed by Thierry Arnoux, 14-Apr-2019.) (Proof shortened by Wolf Lammen, 21-Apr-2024.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) ↔ ((𝜑 ∧ 𝜏 ∧ 𝜌) ∧ ((𝜓 ∧ 𝜃) ∧ (𝜂 ∧ 𝜎) ∧ (𝜒 ∧ 𝜁))))
Theorem	3orel2 1515	Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Eric Schmidt, 8-Oct-2025.)
⊢ (¬ 𝜓 → ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜒)))
Theorem	3orel2OLD 1516	Obsolete version of 3orel2 1515 as of 8-Oct-2025. (Contributed by Scott Fenton, 26-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝜓 → ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜒)))
Theorem	3orel3 1517	Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.)
⊢ (¬ 𝜒 → ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜓)))
Theorem	3orel13 1518	Elimination of two disjuncts in a triple disjunction. (Contributed by Scott Fenton, 9-Jun-2011.)
⊢ ((¬ 𝜑 ∧ ¬ 𝜒) → ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜓))
Theorem	3pm3.2ni 1519	Triple negated disjunction introduction. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ ¬ 𝜑    &   ⊢ ¬ 𝜓    &   ⊢ ¬ 𝜒    ⇒   ⊢ ¬ (𝜑 ∨ 𝜓 ∨ 𝜒)
Theorem	an42ds 1520	Inference exchanging the last antecedent with the second one. See also an32s 664. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜒) ∧ 𝜓) → 𝜏)
1.2.12  Logical "nand" (Sheffer stroke)
Syntax	wnan 1521	Extend wff definition to include alternative denial ("nand").
wff (𝜑 ⊼ 𝜓)
Definition	df-nan 1522	Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1524 for an alternative. This is also called the Sheffer stroke, represented by a vertical bar, but we use a different symbol to avoid ambiguity with other uses of the vertical bar. In the second edition of Principia Mathematica (1927), Russell and Whitehead used the Sheffer stroke and suggested it as a replacement for the "or" and "not" operations of the first edition. However, in practice, "or" and "not" are more widely used. After we define the constant true ⊤ (df-tru 1573) and the constant false ⊥ (df-fal 1583), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1611), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1612), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1613), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1614). Contrast with ∧ (df-an 401), ∨ (df-or 861), → (wi 4), and ⊻ (df-xor 1542). (Contributed by Jeff Hoffman, 19-Nov-2007.)
⊢ ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
Theorem	nanan 1523	Conjunction in terms of alternative denial. (Contributed by Mario Carneiro, 9-May-2015.)
⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 ⊼ 𝜓))
Theorem	dfnan2 1524	Alternative denial in terms of our primitive connectives (implication and negation). (Contributed by WL, 26-Jun-2020.)
⊢ ((𝜑 ⊼ 𝜓) ↔ (𝜑 → ¬ 𝜓))
Theorem	nanor 1525	Alternative denial in terms of disjunction and negation. This explains the name "alternative denial". (Contributed by BJ, 19-Oct-2022.)
⊢ ((𝜑 ⊼ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	nancom 1526	Alternative denial is commutative. Remark: alternative denial is not associative, see nanass 1540. (Contributed by Mario Carneiro, 9-May-2015.) (Proof shortened by Wolf Lammen, 26-Jun-2020.)
⊢ ((𝜑 ⊼ 𝜓) ↔ (𝜓 ⊼ 𝜑))
Theorem	nannan 1527	Nested alternative denials. (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof shortened by Wolf Lammen, 26-Jun-2020.)
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒)))
Theorem	nanim 1528	Implication in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜓)))
Theorem	nannot 1529	Negation in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007.) Use dfnan2 1524. (Revised by Wolf Lammen, 26-Jun-2020.)
⊢ (¬ 𝜑 ↔ (𝜑 ⊼ 𝜑))
Theorem	nanbi 1530	Biconditional in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof shortened by Wolf Lammen, 27-Jun-2020.)
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜑) ⊼ (𝜓 ⊼ 𝜓))))
Theorem	nanbi1 1531	Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by Anthony Hart, 1-Sep-2011.) (Proof shortened by Wolf Lammen, 27-Jun-2020.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜒)))
Theorem	nanbi2 1532	Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by Anthony Hart, 1-Sep-2011.) (Proof shortened by SF, 2-Jan-2018.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ⊼ 𝜑) ↔ (𝜒 ⊼ 𝜓)))
Theorem	nanbi12 1533	Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜃)))
Theorem	nanbi1i 1534	Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜒))
Theorem	nanbi2i 1535	Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ⊼ 𝜑) ↔ (𝜒 ⊼ 𝜓))
Theorem	nanbi12i 1536	Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜃))
Theorem	nanbi1d 1537	Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ⊼ 𝜃) ↔ (𝜒 ⊼ 𝜃)))
Theorem	nanbi2d 1538	Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ⊼ 𝜓) ↔ (𝜃 ⊼ 𝜒)))
Theorem	nanbi12d 1539	Join two logical equivalences with anti-conjunction. (Contributed by Scott Fenton, 2-Jan-2018.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ⊼ 𝜃) ↔ (𝜒 ⊼ 𝜏)))
Theorem	nanass 1540	A characterization of when an expression involving alternative denials associates. Remark: alternative denial is commutative, see nancom 1526. (Contributed by Richard Penner, 29-Feb-2020.) (Proof shortened by Wolf Lammen, 23-Oct-2022.)
⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))
1.2.13  Logical "xor"
Syntax	wxo 1541	Extend wff definition to include exclusive disjunction ("xor").
wff (𝜑 ⊻ 𝜓)
Definition	df-xor 1542	Define exclusive disjunction (logical "xor"). Return true if either the left or right, but not both, are true. After we define the constant true ⊤ (df-tru 1573) and the constant false ⊥ (df-fal 1583), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1615), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1616), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1617), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1618). Contrast with ∧ (df-an 401), ∨ (df-or 861), → (wi 4), and ⊼ (df-nan 1522). (Contributed by FL, 22-Nov-2010.)
⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))
Theorem	xnor 1543	Two ways to write XNOR (exclusive not-or). (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ ((𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ⊻ 𝜓))
Theorem	xorcom 1544	The connector ⊻ is commutative. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 21-Apr-2024.)
⊢ ((𝜑 ⊻ 𝜓) ↔ (𝜓 ⊻ 𝜑))
Theorem	xorass 1545	The connector ⊻ is associative. (Contributed by FL, 22-Nov-2010.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Proof shortened by Wolf Lammen, 20-Jun-2020.)
⊢ (((𝜑 ⊻ 𝜓) ⊻ 𝜒) ↔ (𝜑 ⊻ (𝜓 ⊻ 𝜒)))
Theorem	excxor 1546	This tautology shows that xor is really exclusive. (Contributed by FL, 22-Nov-2010.)
⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓)))
Theorem	xor2 1547	Two ways to express "exclusive or". (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)))
Theorem	xoror 1548	Exclusive disjunction implies disjunction ("XOR implies OR"). (Contributed by BJ, 19-Apr-2019.)
⊢ ((𝜑 ⊻ 𝜓) → (𝜑 ∨ 𝜓))
Theorem	xornan 1549	Exclusive disjunction implies alternative denial ("XOR implies NAND"). (Contributed by BJ, 19-Apr-2019.)
⊢ ((𝜑 ⊻ 𝜓) → ¬ (𝜑 ∧ 𝜓))
Theorem	xornan2 1550	XOR implies NAND (written with the ⊼ connector). (Contributed by BJ, 19-Apr-2019.)
⊢ ((𝜑 ⊻ 𝜓) → (𝜑 ⊼ 𝜓))
Theorem	xorneg2 1551	The connector ⊻ is negated under negation of one argument. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 27-Jun-2020.)
⊢ ((𝜑 ⊻ ¬ 𝜓) ↔ ¬ (𝜑 ⊻ 𝜓))
Theorem	xorneg1 1552	The connector ⊻ is negated under negation of one argument. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 27-Jun-2020.)
⊢ ((¬ 𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ⊻ 𝜓))
Theorem	xorneg 1553	The connector ⊻ is unchanged under negation of both arguments. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ ((¬ 𝜑 ⊻ ¬ 𝜓) ↔ (𝜑 ⊻ 𝜓))
Theorem	xorbi12i 1554	Equality property for exclusive disjunction. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 21-Apr-2024.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ⊻ 𝜒) ↔ (𝜓 ⊻ 𝜃))
Theorem	xorbi12d 1555	Equality property for exclusive disjunction. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ⊻ 𝜃) ↔ (𝜒 ⊻ 𝜏)))
Theorem	anxordi 1556	Conjunction distributes over exclusive-or. In intuitionistic logic this assertion is also true, even though xordi 1034 does not necessarily hold, in part because the usual definition of xor is subtly different in intuitionistic logic. (Contributed by David A. Wheeler, 7-Oct-2018.)
⊢ ((𝜑 ∧ (𝜓 ⊻ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ⊻ (𝜑 ∧ 𝜒)))
Theorem	xorexmid 1557	Exclusive-or variant of the law of the excluded middle (exmid 907). This statement is ancient, going back to at least Stoic logic. This statement does not necessarily hold in intuitionistic logic. (Contributed by David A. Wheeler, 23-Feb-2019.)
⊢ (𝜑 ⊻ ¬ 𝜑)
1.2.14  Logical "nor"
Syntax	wnor 1558	Extend wff definition to include joint denial ("nor").
wff (𝜑 ⊽ 𝜓)
Definition	df-nor 1559	Define joint denial ("not-or" or "nor"). After we define the constant true ⊤ (df-tru 1573) and the constant false ⊥ (df-fal 1583), we will be able to prove these truth table values: ((⊤ ⊽ ⊤) ↔ ⊥) (trunortru 1619), ((⊤ ⊽ ⊥) ↔ ⊥) (trunorfal 1620), ((⊥ ⊽ ⊤) ↔ ⊥) (falnortru 1621), and ((⊥ ⊽ ⊥) ↔ ⊤) (falnorfal 1622). Contrast with ∧ (df-an 401), ∨ (df-or 861), → (wi 4), ⊼ (df-nan 1522), and ⊻ (df-xor 1542). (Contributed by Remi, 25-Oct-2023.)
⊢ ((𝜑 ⊽ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))
Theorem	norcom 1560	The connector ⊽ is commutative. (Contributed by Remi, 25-Oct-2023.) (Proof shortened by Wolf Lammen, 23-Apr-2024.)
⊢ ((𝜑 ⊽ 𝜓) ↔ (𝜓 ⊽ 𝜑))
Theorem	nornot 1561	¬ is expressible via ⊽. (Contributed by Remi, 25-Oct-2023.) (Proof shortened by Wolf Lammen, 8-Dec-2023.)
⊢ (¬ 𝜑 ↔ (𝜑 ⊽ 𝜑))
Theorem	noran 1562	∧ is expressible via ⊽. (Contributed by Remi, 26-Oct-2023.) (Proof shortened by Wolf Lammen, 8-Dec-2023.)
⊢ ((𝜑 ∧ 𝜓) ↔ ((𝜑 ⊽ 𝜑) ⊽ (𝜓 ⊽ 𝜓)))
Theorem	noror 1563	∨ is expressible via ⊽. (Contributed by Remi, 26-Oct-2023.) (Proof shortened by Wolf Lammen, 8-Dec-2023.)
⊢ ((𝜑 ∨ 𝜓) ↔ ((𝜑 ⊽ 𝜓) ⊽ (𝜑 ⊽ 𝜓)))
Theorem	norasslem1 1564	This lemma shows the equivalence of two expressions, used in norass 1567. (Contributed by Wolf Lammen, 18-Dec-2023.)
⊢ (((𝜑 ∨ 𝜓) → 𝜒) ↔ ((𝜑 ⊽ 𝜓) ∨ 𝜒))
Theorem	norasslem2 1565	This lemma specializes biimt 363 suitably for the proof of norass 1567. (Contributed by Wolf Lammen, 18-Dec-2023.)
⊢ (𝜑 → (𝜓 ↔ ((𝜑 ∨ 𝜒) → 𝜓)))
Theorem	norasslem3 1566	This lemma specializes biorf 949 suitably for the proof of norass 1567. (Contributed by Wolf Lammen, 18-Dec-2023.)
⊢ (¬ 𝜑 → ((𝜓 → 𝜒) ↔ ((𝜑 ∨ 𝜓) → 𝜒)))
Theorem	norass 1567	A characterization of when an expression involving joint denials associates. This is identical to the case when alternative denial is associative, see nanass 1540. Remark: Like alternative denial, joint denial is also commutative, see norcom 1560. (Contributed by RP, 29-Oct-2023.) (Proof shortened by Wolf Lammen, 17-Dec-2023.)
⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜑 ⊽ (𝜓 ⊽ 𝜒))))
1.2.15  True and false constants
1.2.15.1  Universal quantifier for use by df-tru Even though it is not ordinarily part of propositional calculus, the universal quantifier ∀ is introduced here so that the soundness of Definition df-tru 1573 can be checked by the same algorithm that is used for predicate calculus. Its first real use is in Definition df-ex 1810 in the predicate calculus section below. For those who want propositional calculus to be self-contained, i.e., to use wff variables only, the alternate Definition dftru2 1575 may be adopted and this subsection moved down to the start of the subsection with wex 1809 below. However, the use of dftru2 1575 as a definition requires a more elaborate definition checking algorithm that we prefer to avoid.
Syntax	wal 1568	Extend wff definition to include the universal quantifier ("for all"). ∀𝑥𝜑 is read "𝜑 (phi) is true for all 𝑥". Typically, in its final application 𝜑 would be replaced with a wff containing a (free) occurrence of the variable 𝑥, for example 𝑥 = 𝑦. In a universe with a finite number of objects, "for all" is equivalent to a big conjunction (AND) with one wff for each possible case of 𝑥. When the universe is infinite (as with set theory), such a propositional-calculus equivalent is not possible because an infinitely long formula has no meaning, but conceptually the idea is the same.
wff ∀𝑥𝜑
1.2.15.2  Equality predicate for use by df-tru Even though it is not ordinarily part of propositional calculus, the equality predicate = is introduced here so that the soundness of definition df-tru 1573 can be checked by the same algorithm as is used for predicate calculus. Its first real use is in Theorem weq 1992 in the predicate calculus section below. For those who want propositional calculus to be self-contained, i.e., to use wff variables only, the alternate definition dftru2 1575 may be adopted and this subsection moved down to just above weq 1992 below. However, the use of dftru2 1575 as a definition requires a more elaborate definition checking algorithm that we prefer to avoid.
Syntax	cv 1569	This syntax construction states that a variable 𝑥, which has been declared to be a setvar variable by $f statement vx, is also a class expression. This can be justified informally as follows. We know that the class builder {𝑦 ∣ 𝑦 ∈ 𝑥} is a class by cab 2741. Since (when 𝑦 is distinct from 𝑥) we have 𝑥 = {𝑦 ∣ 𝑦 ∈ 𝑥} by cvjust 2757, we can argue that the syntax "class 𝑥 " can be viewed as an abbreviation for "class {𝑦 ∣ 𝑦 ∈ 𝑥}". See the discussion under the definition of class in [Jech] p. 4 showing that "Every set can be considered to be a class". While it is tempting and perhaps occasionally useful to view cv 1569 as a "type conversion" from a setvar variable to a class variable, keep in mind that cv 1569 is intrinsically no different from any other class-building syntax such as cab 2741, cun 3904, or c0 4287. For a general discussion of the theory of classes and the role of cv 1569, see mmset.html#class 1569. (The description above applies to set theory, not predicate calculus. The purpose of introducing class 𝑥 here, and not in set theory where it belongs, is to allow to express, i.e., "prove", the weq 1992 of predicate calculus from the wceq 1570 of set theory, so that we do not overload the = connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers.)
class 𝑥
Syntax	wceq 1570	Extend wff definition to include class equality. For a general discussion of the theory of classes, see mmset.html#class. (The purpose of introducing wff 𝐴 = 𝐵 here, and not in set theory where it belongs, is to allow to express, i.e., "prove", the weq 1992 of predicate calculus in terms of the wceq 1570 of set theory, so that we do not "overload" the = connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers. For example, some parsers - although not the Metamath program - stumble on the fact that the = in 𝑥 = 𝑦 could be the = of either weq 1992 or wceq 1570, although mathematically it makes no difference. The class variables 𝐴 and 𝐵 are introduced temporarily for the purpose of this definition but otherwise not used in predicate calculus. See df-cleq 2755 for more information on the set theory usage of wceq 1570.)
wff 𝐴 = 𝐵
1.2.15.3  The true constant
Syntax	wtru 1571	The constant ⊤ is a wff.
wff ⊤
Theorem	trujust 1572	Soundness justification theorem for df-tru 1573. Instance of monothetic 269. (Contributed by Mario Carneiro, 17-Nov-2013.) (Revised by NM, 11-Jul-2019.)
⊢ ((∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥) ↔ (∀𝑦 𝑦 = 𝑦 → ∀𝑦 𝑦 = 𝑦))
Definition	df-tru 1573	Definition of the truth value "true", or "verum", denoted by ⊤. In this definition, an instance of id 23 is used as the definiens, although any tautology, such as an axiom, can be used in its place. This particular instance of id 23 was chosen so this definition can be checked by the same algorithm that is used for predicate calculus. This definition should be referenced directly only by tru 1574, and other proofs should use tru 1574 instead of this definition, since there are many alternate ways to define ⊤. (Contributed by Anthony Hart, 13-Oct-2010.) (Revised by NM, 11-Jul-2019.) Use tru 1574 instead. (New usage is discouraged.)
⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
Theorem	tru 1574	The truth value ⊤ is provable. (Contributed by Anthony Hart, 13-Oct-2010.)
⊢ ⊤
Theorem	dftru2 1575	An alternate definition of "true" (see comment of df-tru 1573). The associated justification theorem is monothetic 269. (Contributed by Anthony Hart, 13-Oct-2010.) (Revised by BJ, 12-Jul-2019.) Use tru 1574 instead. (New usage is discouraged.)
⊢ (⊤ ↔ (𝜑 → 𝜑))
Theorem	trut 1576	A proposition is equivalent to it being implied by ⊤. Closed form of mptru 1577. Dual of dfnot 1589. It is to tbtru 1578 what a1bi 365 is to tbt 372. (Contributed by BJ, 26-Oct-2019.)
⊢ (𝜑 ↔ (⊤ → 𝜑))
Theorem	mptru 1577	Eliminate ⊤ as an antecedent. A proposition implied by ⊤ is true. This is modus ponens ax-mp 5 when the minor hypothesis is ⊤ (which holds by tru 1574). (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (⊤ → 𝜑)    ⇒   ⊢ 𝜑
Theorem	tbtru 1578	A proposition is equivalent to itself being equivalent to ⊤. (Contributed by Anthony Hart, 14-Aug-2011.)
⊢ (𝜑 ↔ (𝜑 ↔ ⊤))
Theorem	bitru 1579	A theorem is equivalent to truth. (Contributed by Mario Carneiro, 9-May-2015.)
⊢ 𝜑    ⇒   ⊢ (𝜑 ↔ ⊤)
Theorem	trud 1580	Anything implies ⊤. Dual statement of falim 1587. Deduction form of tru 1574. Note on naming: in 2022, the theorem now known as mptru 1577 was renamed from trud so if you are reading documentation written before that time, references to trud refer to what is now mptru 1577. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.)
⊢ (𝜑 → ⊤)
Theorem	truan 1581	True can be removed from a conjunction. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Wolf Lammen, 21-Jul-2019.)
⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)
1.2.15.4  The false constant
Syntax	wfal 1582	The constant ⊥ is a wff.
wff ⊥
Definition	df-fal 1583	Definition of the truth value "false", or "falsum", denoted by ⊥. See also df-tru 1573. (Contributed by Anthony Hart, 22-Oct-2010.)
⊢ (⊥ ↔ ¬ ⊤)
Theorem	fal 1584	The truth value ⊥ is refutable. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Mel L. O'Cat, 11-Mar-2012.)
⊢ ¬ ⊥
Theorem	nbfal 1585	The negation of a proposition is equivalent to itself being equivalent to ⊥. (Contributed by Anthony Hart, 14-Aug-2011.)
⊢ (¬ 𝜑 ↔ (𝜑 ↔ ⊥))
Theorem	bifal 1586	A contradiction is equivalent to falsehood. (Contributed by Mario Carneiro, 9-May-2015.)
⊢ ¬ 𝜑    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	falim 1587	The truth value ⊥ implies anything. Also called the "principle of explosion", or "ex falso [sequitur]] quodlibet" (Latin for "from falsehood, anything [follows]]"). Dual statement of trud 1580. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.)
⊢ (⊥ → 𝜑)
Theorem	falimd 1588	The truth value ⊥ implies anything. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ ((𝜑 ∧ ⊥) → 𝜓)
Theorem	dfnot 1589	Given falsum ⊥, we can define the negation of a wff 𝜑 as the statement that ⊥ follows from assuming 𝜑. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 21-Jul-2019.)
⊢ (¬ 𝜑 ↔ (𝜑 → ⊥))
Theorem	inegd 1590	Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ ((𝜑 ∧ 𝜓) → ⊥)    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	efald 1591	Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ ((𝜑 ∧ ¬ 𝜓) → ⊥)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.21fal 1592	If a wff and its negation are provable, then falsum is provable. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ⊥)
1.2.16  Truth tables Some sources define logical connectives by their truth tables. These are tables that give the truth value of the composed expression for all possible combinations of the truth values of their arguments. In this section, we show that our definitions and axioms produce equivalent results for all the logical connectives we have introduced (either axiomatically or by a definition): implication wi 4, negation wn 3, biconditional df-bi 210, conjunction df-an 401, disjunction df-or 861, alternative denial df-nan 1522, exclusive disjunction df-xor 1542.
1.2.16.1  Implication
Theorem	truimtru 1593	A → identity. (Contributed by Anthony Hart, 22-Oct-2010.) An alternate proof is possible using trud 1580 instead of id 23 but the principle of identity id 23 is more basic, and the present proof indicates that the result still holds in relevance logic. (Proof modification is discouraged.)
⊢ ((⊤ → ⊤) ↔ ⊤)
Theorem	truimfal 1594	A → identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ ((⊤ → ⊥) ↔ ⊥)
Theorem	falimtru 1595	A → identity. (Contributed by Anthony Hart, 22-Oct-2010.) An alternate proof is possible using falim 1587 instead of trud 1580 but the present proof using trud 1580 emphasizes that the result does not require the principle of explosion. (Proof modification is discouraged.)
⊢ ((⊥ → ⊤) ↔ ⊤)
Theorem	falimfal 1596	A → identity. (Contributed by Anthony Hart, 22-Oct-2010.) An alternate proof is possible using falim 1587 instead of id 23 but the present proof using id 23 emphasizes that the result does not require the principle of explosion. (Proof modification is discouraged.)
⊢ ((⊥ → ⊥) ↔ ⊤)
1.2.16.2  Negation
Theorem	nottru 1597	A ¬ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
⊢ (¬ ⊤ ↔ ⊥)
Theorem	notfal 1598	A ¬ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ (¬ ⊥ ↔ ⊤)
1.2.16.3  Equivalence
Theorem	trubitru 1599	A ↔ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ ((⊤ ↔ ⊤) ↔ ⊤)
Theorem	falbitru 1600	A ↔ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 10-Jul-2020.)
⊢ ((⊥ ↔ ⊤) ↔ ⊥)