Metamath Proof Explorer - mmtheorems5

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 401-500 - Page 5 of 58

Type	Label	Description
Statement
Theorem	bicon4i 401	A contraposition inference.
⊢ (¬ φ ↔ ¬ ψ)    ⇒   ⊢ (φ ↔ ψ)
Theorem	bicon4d 402	A contraposition deduction.
⊢ (φ → (¬ ψ ↔ ¬ χ))    ⇒   ⊢ (φ → (ψ ↔ χ))
Theorem	bicon2 403	Contraposition. Theorem *4.12 of [WhiteheadRussell] p. 117.
⊢ ((φ ↔ ¬ ψ) ↔ (ψ ↔ ¬ φ))
Theorem	bicon2d 404	A contraposition deduction.
⊢ (φ → (ψ ↔ ¬ χ))    ⇒   ⊢ (φ → (χ ↔ ¬ ψ))
Theorem	bicon1d 405	A contraposition deduction.
⊢ (φ → (¬ ψ ↔ χ))    ⇒   ⊢ (φ → (¬ χ ↔ ψ))
Theorem	bitrd 406	Deduction form of bitr 151.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (χ ↔ θ))    ⇒   ⊢ (φ → (ψ ↔ θ))
Theorem	bitr2d 407	Deduction form of bitr2 152.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (χ ↔ θ))    ⇒   ⊢ (φ → (θ ↔ ψ))
Theorem	bitr3d 408	Deduction form of bitr3 153.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (ψ ↔ θ))    ⇒   ⊢ (φ → (χ ↔ θ))
Theorem	bitr4d 409	Deduction form of bitr4 154.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ χ))    ⇒   ⊢ (φ → (ψ ↔ θ))
Theorem	syl5bb 410	A syllogism inference from two biconditionals.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ ↔ ψ)    ⇒   ⊢ (φ → (θ ↔ χ))
Theorem	syl5rbb 411	A syllogism inference from two biconditionals.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ ↔ ψ)    ⇒   ⊢ (φ → (χ ↔ θ))
Theorem	syl5bbr 412	A syllogism inference from two biconditionals.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (ψ ↔ θ)    ⇒   ⊢ (φ → (θ ↔ χ))
Theorem	syl5rbbr 413	A syllogism inference from two biconditionals.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (ψ ↔ θ)    ⇒   ⊢ (φ → (χ ↔ θ))
Theorem	syl6bb 414	A syllogism inference from two biconditionals.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (χ ↔ θ)    ⇒   ⊢ (φ → (ψ ↔ θ))
Theorem	syl6rbb 415	A syllogism inference from two biconditionals.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (χ ↔ θ)    ⇒   ⊢ (φ → (θ ↔ ψ))
Theorem	syl6bbr 416	A syllogism inference from two biconditionals.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ ↔ χ)    ⇒   ⊢ (φ → (ψ ↔ θ))
Theorem	syl6rbbr 417	A syllogism inference from two biconditionals.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ ↔ χ)    ⇒   ⊢ (φ → (θ ↔ ψ))
Theorem	sylan9bb 418	Nested syllogism inference conjoining dissimilar antecedents.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ → (χ ↔ τ))    ⇒   ⊢ ((φ ∧ θ) → (ψ ↔ τ))
Theorem	sylan9bbr 419	Nested syllogism inference conjoining dissimilar antecedents.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ → (χ ↔ τ))    ⇒   ⊢ ((θ ∧ φ) → (ψ ↔ τ))
Theorem	3imtr3d 420	More general version of 3imtr3 191. Useful for converting conditional definitions in a formula.
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (ψ ↔ θ))    &   ⊢ (φ → (χ ↔ τ))    ⇒   ⊢ (φ → (θ → τ))
Theorem	3imtr4d 421	More general version of 3imtr4 192. Useful for converting conditional definitions in a formula.
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (θ ↔ ψ))    &   ⊢ (φ → (τ ↔ χ))    ⇒   ⊢ (φ → (θ → τ))
Theorem	3bitrd 422	Deduction from transitivity of biconditional.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (χ ↔ θ))    &   ⊢ (φ → (θ ↔ τ))    ⇒   ⊢ (φ → (ψ ↔ τ))
Theorem	3bitr3d 423	Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (ψ ↔ θ))    &   ⊢ (φ → (χ ↔ τ))    ⇒   ⊢ (φ → (θ ↔ τ))
Theorem	3bitr4d 424	Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ ψ))    &   ⊢ (φ → (τ ↔ χ))    ⇒   ⊢ (φ → (θ ↔ τ))
Theorem	3imtr3g 425	More general version of 3imtr3 191. Useful for converting definitions in a formula.
⊢ (φ → (ψ → χ))    &   ⊢ (ψ ↔ θ)    &   ⊢ (χ ↔ τ)    ⇒   ⊢ (φ → (θ → τ))
Theorem	3imtr4g 426	More general version of 3imtr4 192. Useful for converting definitions in a formula.
⊢ (φ → (ψ → χ))    &   ⊢ (θ ↔ ψ)    &   ⊢ (τ ↔ χ)    ⇒   ⊢ (φ → (θ → τ))
Theorem	3bitr3g 427	More general version of 3bitr3 156. Useful for converting definitions in a formula.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (ψ ↔ θ)    &   ⊢ (χ ↔ τ)    ⇒   ⊢ (φ → (θ ↔ τ))
Theorem	3bitr4g 428	More general version of 3bitr4 158. Useful for converting definitions in a formula.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ ↔ ψ)    &   ⊢ (τ ↔ χ)    ⇒   ⊢ (φ → (θ ↔ τ))
Theorem	prth 429	Theorem *3.47 of [WhiteheadRussell] p. 113. It was proved by Leibniz, and it evidently pleased him enough to call it 'praeclarum theorema.'
⊢ (((φ → ψ) ∧ (χ → θ)) → ((φ ∧ χ) → (ψ ∧ θ)))
Theorem	pm3.48 430	Theorem *3.48 of [WhiteheadRussell] p. 114.
⊢ (((φ → ψ) ∧ (χ → θ)) → ((φ ∨ χ) → (ψ ∨ θ)))
Theorem	anim12d 431	Conjoin antecedents and consequents in a deduction.
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (θ → τ))    ⇒   ⊢ (φ → ((ψ ∧ θ) → (χ ∧ τ)))
Theorem	anim1d 432	Add a conjunct to right of antecedent and consequent in a deduction.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → ((ψ ∧ θ) → (χ ∧ θ)))
Theorem	anim2d 433	Add a conjunct to left of antecedent and consequent in a deduction.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → ((θ ∧ ψ) → (θ ∧ χ)))
Theorem	im2anan9 434	Deduction joining nested implications to form implication of conjunctions.
⊢ (φ → (ψ → χ))    &   ⊢ (θ → (τ → η))    ⇒   ⊢ ((φ ∧ θ) → ((ψ ∧ τ) → (χ ∧ η)))
Theorem	im2anan9r 435	Deduction joining nested implications to form implication of conjunctions.
⊢ (φ → (ψ → χ))    &   ⊢ (θ → (τ → η))    ⇒   ⊢ ((θ ∧ φ) → ((ψ ∧ τ) → (χ ∧ η)))
Theorem	orim12d 436	Disjoin antecedents and consequents in a deduction.
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (θ → τ))    ⇒   ⊢ (φ → ((ψ ∨ θ) → (χ ∨ τ)))
Theorem	orim1d 437	Disjoin antecedents and consequents in a deduction.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → ((ψ ∨ θ) → (χ ∨ θ)))
Theorem	orim2d 438	Disjoin antecedents and consequents in a deduction.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → ((θ ∨ ψ) → (θ ∨ χ)))
Theorem	pm2.85 439	Theorem *2.85 of [WhiteheadRussell] p. 108.
⊢ (((φ ∨ ψ) → (φ ∨ χ)) → (φ ∨ (ψ → χ)))
Theorem	pm3.2ni 440	Infer negated disjunction of negated premises.
⊢ ¬ φ    &   ⊢ ¬ ψ    ⇒   ⊢ ¬ (φ ∨ ψ)
Theorem	oel 441	Elimination of redundant internal disjunct. Compare Theorem *4.45 of [WhiteheadRussell] p. 119.
⊢ (φ ↔ ((φ ∨ ψ) ∧ φ))
Theorem	pm5.74 442	Distribution of implication over biconditional. Theorem *5.74 of [WhiteheadRussell] p. 126.
⊢ ((φ → (ψ ↔ χ)) ↔ ((φ → ψ) ↔ (φ → χ)))
Theorem	pm5.74i 443	Distribution of implication over biconditional (inference rule).
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ ((φ → ψ) ↔ (φ → χ))
Theorem	pm5.74d 444	Distribution of implication over biconditional (deduction rule).
⊢ (φ → (ψ → (χ ↔ θ)))    ⇒   ⊢ (φ → ((ψ → χ) ↔ (ψ → θ)))
Theorem	pm5.74ri 445	Distribution of implication over biconditional (reverse inference rule).
⊢ ((φ → ψ) ↔ (φ → χ))    ⇒   ⊢ (φ → (ψ ↔ χ))
Theorem	pm5.74rd 446	Distribution of implication over biconditional (deduction rule).
⊢ (φ → ((ψ → χ) ↔ (ψ → θ)))    ⇒   ⊢ (φ → (ψ → (χ ↔ θ)))
Theorem	mpbidi 447	A deduction from a biconditional, related to modus ponens.
⊢ (θ → (φ → ψ))    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (θ → (φ → χ))
Theorem	ibib 448	Implication in terms of implication and biconditional.
⊢ ((φ → ψ) ↔ (φ → (φ ↔ ψ)))
Theorem	ibi 449	Inference that converts a biconditional implied by one of its arguments, into an implication.
⊢ (φ → (φ ↔ ψ))    ⇒   ⊢ (φ → ψ)
Theorem	ibir 450	Inference that converts a biconditional implied by one of its arguments, into an implication.
⊢ (φ → (ψ ↔ φ))    ⇒   ⊢ (φ → ψ)
Theorem	ibd 451	Deduction that converts a biconditional implied by one of its arguments, into an implication.
⊢ (φ → (ψ → (ψ ↔ χ)))    ⇒   ⊢ (φ → (ψ → χ))
Theorem	ordi 452	Distributive law for disjunction. Theorem *4.41 of [WhiteheadRussell] p. 119.
⊢ ((φ ∨ (ψ ∧ χ)) ↔ ((φ ∨ ψ) ∧ (φ ∨ χ)))
Theorem	ordir 453	Distributive law for disjunction.
⊢ (((φ ∧ ψ) ∨ χ) ↔ ((φ ∨ χ) ∧ (ψ ∨ χ)))
Theorem	jcab 454	Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121.
⊢ ((φ → (ψ ∧ χ)) ↔ ((φ → ψ) ∧ (φ → χ)))
Theorem	jcad 455	Deduction conjoining the consequents of two implications.
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (ψ → θ))    ⇒   ⊢ (φ → (ψ → (χ ∧ θ)))
Theorem	andi 456	Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118.
⊢ ((φ ∧ (ψ ∨ χ)) ↔ ((φ ∧ ψ) ∨ (φ ∧ χ)))
Theorem	andir 457	Distributive law for conjunction.
⊢ (((φ ∨ ψ) ∧ χ) ↔ ((φ ∧ χ) ∨ (ψ ∧ χ)))
Theorem	orddi 458	Double distributive law for disjunction.
⊢ (((φ ∧ ψ) ∨ (χ ∧ θ)) ↔ (((φ ∨ χ) ∧ (φ ∨ θ)) ∧ ((ψ ∨ χ) ∧ (ψ ∨ θ))))
Theorem	anddi 459	Double distributive law for conjunction.
⊢ (((φ ∨ ψ) ∧ (χ ∨ θ)) ↔ (((φ ∧ χ) ∨ (φ ∧ θ)) ∨ ((ψ ∧ χ) ∨ (ψ ∧ θ))))
Theorem	bibi2i 460	Inference adding a biconditional to the left in an equivalence.
⊢ (φ ↔ ψ)    ⇒   ⊢ ((χ ↔ φ) ↔ (χ ↔ ψ))
Theorem	bibi1i 461	Inference adding a biconditional to the right in an equivalence.
⊢ (φ ↔ ψ)    ⇒   ⊢ ((φ ↔ χ) ↔ (ψ ↔ χ))
Theorem	bibi12i 462	The equivalence of two equivalences.
⊢ (φ ↔ ψ)    &   ⊢ (χ ↔ θ)    ⇒   ⊢ ((φ ↔ χ) ↔ (ψ ↔ θ))
Theorem	negbid 463	Deduction negating both sides of a logical equivalence.
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (¬ ψ ↔ ¬ χ))
Theorem	imbi2d 464	Deduction adding an antecedent to both sides of a logical equivalence.
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ((θ → ψ) ↔ (θ → χ)))
Theorem	imbi1d 465	Deduction adding a consequent to both sides of a logical equivalence.
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ((ψ → θ) ↔ (χ → θ)))
Theorem	orbi2d 466	Deduction adding a left disjunct to both sides of a logical equivalence.
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ((θ ∨ ψ) ↔ (θ ∨ χ)))
Theorem	orbi1d 467	Deduction adding a right disjunct to both sides of a logical equivalence.
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ((ψ ∨ θ) ↔ (χ ∨ θ)))
Theorem	anbi2d 468	Deduction adding a left conjunct to both sides of a logical equivalence.
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ((θ ∧ ψ) ↔ (θ ∧ χ)))
Theorem	anbi1d 469	Deduction adding a right conjunct to both sides of a logical equivalence.
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ((ψ ∧ θ) ↔ (χ ∧ θ)))
Theorem	bibi2d 470	Deduction adding a biconditional to the left in an equivalence.
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ((θ ↔ ψ) ↔ (θ ↔ χ)))
Theorem	bibi1d 471	Deduction adding a biconditional to the right in an equivalence.
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ((ψ ↔ θ) ↔ (χ ↔ θ)))
Theorem	imbi1 472	Theorem *4.84 of [WhiteheadRussell] p. 122.
⊢ ((φ ↔ ψ) → ((φ → χ) ↔ (ψ → χ)))
Theorem	imbi2 473	Theorem *4.85 of [WhiteheadRussell] p. 122.
⊢ ((φ ↔ ψ) → ((χ → φ) ↔ (χ → ψ)))
Theorem	imbi12d 474	Deduction joining two equivalences to form equivalence of implications.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ τ))    ⇒   ⊢ (φ → ((ψ → θ) ↔ (χ → τ)))
Theorem	orbi12d 475	Deduction joining two equivalences to form equivalence of disjunctions.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ τ))    ⇒   ⊢ (φ → ((ψ ∨ θ) ↔ (χ ∨ τ)))
Theorem	anbi12d 476	Deduction joining two equivalences to form equivalence of conjunctions.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ τ))    ⇒   ⊢ (φ → ((ψ ∧ θ) ↔ (χ ∧ τ)))
Theorem	bibi12d 477	Deduction joining two equivalences to form equivalence of biconditionals.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ τ))    ⇒   ⊢ (φ → ((ψ ↔ θ) ↔ (χ ↔ τ)))
Theorem	bi2anan9 478	Deduction joining two equivalences to form equivalence of conjunctions.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ → (τ ↔ η))    ⇒   ⊢ ((φ ∧ θ) → ((ψ ∧ τ) ↔ (χ ∧ η)))
Theorem	bi2anan9r 479	Deduction joining two equivalences to form equivalence of conjunctions.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ → (τ ↔ η))    ⇒   ⊢ ((θ ∧ φ) → ((ψ ∧ τ) ↔ (χ ∧ η)))
Theorem	bi2bian9 480	Deduction joining two biconditionals with different antecedents.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ → (τ ↔ η))    ⇒   ⊢ ((φ ∧ θ) → ((ψ ↔ τ) ↔ (χ ↔ η)))
Theorem	pm4.71 481	Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120.
⊢ ((φ → ψ) ↔ (φ ↔ (φ ∧ ψ)))
Theorem	pm4.71r 482	Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed).
⊢ ((φ → ψ) ↔ (φ ↔ (ψ ∧ φ)))
Theorem	pm4.71i 483	Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120.
⊢ (φ → ψ)    ⇒   ⊢ (φ ↔ (φ ∧ ψ))
Theorem	pm4.71ri 484	Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed).
⊢ (φ → ψ)    ⇒   ⊢ (φ ↔ (ψ ∧ φ))
Theorem	pm4.72 485	Implication in terms of biconditional and disjunction. Theorem *4.72 of [WhiteheadRussell] p. 121.
⊢ ((φ → ψ) ↔ (ψ ↔ (φ ∨ ψ)))
Theorem	iba 486	Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121.
⊢ (φ → (ψ ↔ (ψ ∧ φ)))
Theorem	ibar 487	Introduction of antecedent as conjunct.
⊢ (φ → (ψ ↔ (φ ∧ ψ)))
Theorem	pm5.32 488	Distribution of implication over biconditional. Theorem *5.32 of [WhiteheadRussell] p. 125.
⊢ ((φ → (ψ ↔ χ)) ↔ ((φ ∧ ψ) ↔ (φ ∧ χ)))
Theorem	pm5.32i 489	Distribution of implication over biconditional (inference rule).
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ ((φ ∧ ψ) ↔ (φ ∧ χ))
Theorem	pm5.32ri 490	Distribution of implication over biconditional (inference rule).
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ ((ψ ∧ φ) ↔ (χ ∧ φ))
Theorem	pm5.32d 491	Distribution of implication over biconditional (deduction rule).
⊢ (φ → (ψ → (χ ↔ θ)))    ⇒   ⊢ (φ → ((ψ ∧ χ) ↔ (ψ ∧ θ)))
Theorem	pm5.32rd 492	Distribution of implication over biconditional (deduction rule).
⊢ (φ → (ψ → (χ ↔ θ)))    ⇒   ⊢ (φ → ((χ ∧ ψ) ↔ (θ ∧ ψ)))
Theorem	oibabs 493	Absorption of disjunction into equivalence.
⊢ ((φ ↔ ψ) ↔ ((φ ∨ ψ) → (φ ↔ ψ)))
Theorem	exmid 494	Law of excluded middle. Theorem *2.11 of [WhiteheadRussell] p. 101. It says that something is either true or not true; there are no in-between values of truth. This is an essential distinction of our classical logic and is not a theorem of intuitionistic logic.
⊢ (φ ∨ ¬ φ)
Theorem	pm2.1 495	Theorem *2.1 of [WhiteheadRussell] p. 101.
⊢ (¬ φ ∨ φ)
Theorem	pm3.24 496	Law of contradiction. Theorem *3.24 of [WhiteheadRussell] p. 111.
⊢ ¬ (φ ∧ ¬ φ)
Theorem	pm5.18 497	Theorem *5.18 of [WhiteheadRussell] p. 124. This theorem says that logical equivalence is the same as negated "exclusive-or".
⊢ ((φ ↔ ψ) ↔ ¬ (φ ↔ ¬ ψ))
Theorem	nbbn 498	Move negation outside of biconditional. Compare Theorem *5.18 of [WhiteheadRussell] p. 124.
⊢ ((¬ φ ↔ ψ) ↔ ¬ (φ ↔ ψ))
Theorem	dfbi 499	An alternate definition of the biconditional. Theorem *5.23 of [WhiteheadRussell] p. 124.
⊢ ((φ ↔ ψ) ↔ ((φ ∧ ψ) ∨ (¬ φ ∧ ¬ ψ)))
Theorem	xor 500	Two ways to express "exclusive or". Theorem *5.22 of [WhiteheadRussell] p. 124.
⊢ (¬ (φ ↔ ψ) ↔ ((φ ∧ ¬ ψ) ∨ (ψ ∧ ¬ φ)))