P. 5 of Theorem List - bfol.mm Proof Explorer

Theorem List for bfol.mm Proof Explorer - 401-500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	joinimandres-P4.8b.RC 401	Inference Form of joinimandres-P4.8b 400. †
⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜗))    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜗))
Theorem	joinimandres-P4.8b.CL 402	Closed Form of joinimandres-P4.8b 400. †
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜗)) → ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜗)))
Theorem	joinimor-P4.8c 403	Join Two Implications Through Disjunction. †
⊢ (𝛾 → ((𝜑 → 𝜓) ∨ (𝜒 → 𝜗)))    ⇒   ⊢ (𝛾 → ((𝜑 ∧ 𝜒) → (𝜓 ∨ 𝜗)))
Theorem	joinimor-P4.8c.RC 404	Inference Form of joinimor-P4.8c 403. †
⊢ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜗))    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∨ 𝜗))
Theorem	joinimor-P4.8c.CL 405	Closed Form of joinimor-P4.8c 403. †
⊢ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜗)) → ((𝜑 ∧ 𝜒) → (𝜓 ∨ 𝜗)))
5.1.6  Separating Implications.
Theorem	sepimandr-P4.9a 406	Separate Right Conjunction from Implication. †
⊢ (𝛾 → (𝜑 → (𝜓 ∧ 𝜒)))    ⇒   ⊢ (𝛾 → ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)))
Theorem	sepimandr-P4.9a.RC 407	Inference Form of sepimandr-P4.9a 406. †
⊢ (𝜑 → (𝜓 ∧ 𝜒))    ⇒   ⊢ ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒))
Theorem	sepimandr-P4.9a.CL 408	Closed Form of sepimandr-P4.9a 406. †
⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)))
Theorem	sepimorl-P4.9b 409	Separate Left Disjunction from Implication. †
⊢ (𝛾 → ((𝜑 ∨ 𝜓) → 𝜒))    ⇒   ⊢ (𝛾 → ((𝜑 → 𝜒) ∧ (𝜓 → 𝜒)))
Theorem	sepimorl-P4.9b.RC 410	Inference Form of sepimorl-P4.9b 409. †
⊢ ((𝜑 ∨ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 → 𝜒) ∧ (𝜓 → 𝜒))
Theorem	sepimorl-P4.9b.CL 411	Closed Form of sepimorl-P4.9b 409. †
⊢ (((𝜑 ∨ 𝜓) → 𝜒) → ((𝜑 → 𝜒) ∧ (𝜓 → 𝜒)))
Theorem	sepimorr-P4.9c 412	Separate Right Disjunction from Implication.
⊢ (𝛾 → (𝜑 → (𝜓 ∨ 𝜒)))    ⇒   ⊢ (𝛾 → ((𝜑 → 𝜓) ∨ (𝜑 → 𝜒)))
Theorem	sepimorr-P4.9c.RC 413	Inference Form of sepimorr-P4.9c 412.
⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ ((𝜑 → 𝜓) ∨ (𝜑 → 𝜒))
Theorem	sepimorr-P4.9c.CL 414	Closed Form of sepimorr-P4.9c 412.
⊢ ((𝜑 → (𝜓 ∨ 𝜒)) → ((𝜑 → 𝜓) ∨ (𝜑 → 𝜒)))
Theorem	sepimandl-P4.9d 415	Separate Left Conjunction from Implication.
⊢ (𝛾 → ((𝜑 ∧ 𝜓) → 𝜒))    ⇒   ⊢ (𝛾 → ((𝜑 → 𝜒) ∨ (𝜓 → 𝜒)))
Theorem	sepimandl-P4.9d.RC 416	Inference Form of sepimandl-P4.9d 415.
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 → 𝜒) ∨ (𝜓 → 𝜒))
Theorem	sepimandl-P4.9d.CL 417	Closed Form of sepimandl-P4.9d 415.
⊢ (((𝜑 ∧ 𝜓) → 𝜒) → ((𝜑 → 𝜒) ∨ (𝜓 → 𝜒)))
5.1.7  Some Double Negation Laws.
Theorem	dnegeq-P4.10 418	Double Negation Equivalence Property.
⊢ (¬ ¬ 𝜑 ↔ 𝜑)
Theorem	negbicancel-P4.11 419	Negation Cancellation Rule.
⊢ (𝛾 → (¬ 𝜑 ↔ ¬ 𝜓))    ⇒   ⊢ (𝛾 → (𝜑 ↔ 𝜓))
Theorem	negbicancel-P4.11.RC 420	Inference Form of negbicancel-P4.11 419.
⊢ (¬ 𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	dnegeint-P4.12 421	Version of Double Negative Elimination deducible with intuitionist logic. †
⊢ (𝛾 → ¬ ¬ ¬ 𝜑)    ⇒   ⊢ (𝛾 → ¬ 𝜑)
Theorem	dnegeint-P4.12.RC 422	Inference Form of dnegeint-P4.12 421. †
⊢ ¬ ¬ ¬ 𝜑    ⇒   ⊢ ¬ 𝜑
Theorem	dnegeqint-P4.13 423	Double Negative Equivalence Property deducible with intuitionist logic. †
⊢ (¬ ¬ ¬ 𝜑 ↔ ¬ 𝜑)
Theorem	negbicancelint-P4.14 424	Negation Cancellation Rule derivalbe with intuitionist logic. †
⊢ (𝛾 → (¬ ¬ 𝜑 ↔ ¬ ¬ 𝜓))    ⇒   ⊢ (𝛾 → (¬ 𝜑 ↔ ¬ 𝜓))
Theorem	negbicancelint-P4.14.RC 425	Inference Form of negbicancelint-P4.14 424. †
⊢ (¬ ¬ 𝜑 ↔ ¬ ¬ 𝜓)    ⇒   ⊢ (¬ 𝜑 ↔ ¬ 𝜓)
5.1.8  Extended Syllogism and Transitivity Laws.
Theorem	tsyl-P4.15 426	Triple Syllogism. †
⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → (𝜓 → 𝜒))    &   ⊢ (𝛾 → (𝜒 → 𝜗))    &   ⊢ (𝛾 → (𝜗 → 𝜏))    ⇒   ⊢ (𝛾 → (𝜑 → 𝜏))
Theorem	tsyl-P4.15.RC 427	Inference form of tsyl-P4.15 426. †
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜒 → 𝜗)    &   ⊢ (𝜗 → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	dbitrns-P4.16 428	Doubled Transitive Rule for Biconditional. †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    &   ⊢ (𝛾 → (𝜓 ↔ 𝜒))    &   ⊢ (𝛾 → (𝜒 ↔ 𝜗))    ⇒   ⊢ (𝛾 → (𝜑 ↔ 𝜗))
Theorem	dbitrns-P4.16.RC 429	Inference Form of dbitrns-P4.16 428. †
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    &   ⊢ (𝜒 ↔ 𝜗)    ⇒   ⊢ (𝜑 ↔ 𝜗)
Theorem	tbitrns-P4.17 430	Triple Transitive Rule for Biconditional. †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    &   ⊢ (𝛾 → (𝜓 ↔ 𝜒))    &   ⊢ (𝛾 → (𝜒 ↔ 𝜗))    &   ⊢ (𝛾 → (𝜗 ↔ 𝜏))    ⇒   ⊢ (𝛾 → (𝜑 ↔ 𝜏))
Theorem	tbitrns-P4.17.RC 431	Inference Form of tbitrns-P4.17 430. †
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    &   ⊢ (𝜒 ↔ 𝜗)    &   ⊢ (𝜗 ↔ 𝜏)    ⇒   ⊢ (𝜑 ↔ 𝜏)
5.1.9  Negation Introduction Using "False" Constant. The following scheme is useful for shortening proofs where one must derive an absurdity from each statement within a disjunction in order to show that the entire disjunction is absurd.
5.1.9.1  Rule.
Theorem	falsenegi-P4.18 432	Derived Natural Deduction Rule Using '⊥'. †
⊢ ((𝛾 ∧ 𝜑) → ⊥)    ⇒   ⊢ (𝛾 → ¬ 𝜑)
5.1.9.2  Scheme. These derived rules may be used in place of falsenegi-P4.18 432.
Theorem	rcp-FALSENEGI1 433	'¬' Introduction with '⊥'. †
⊢ (𝛾₁ → ⊥)    ⇒   ⊢ ¬ 𝛾₁
Theorem	rcp-FALSENEGI2 434	'¬' Introduction with '⊥'. †
⊢ ((𝛾₁ ∧ 𝛾₂) → ⊥)    ⇒   ⊢ (𝛾₁ → ¬ 𝛾₂)
Theorem	rcp-FALSENEGI3 435	'¬' Introduction with '⊥'. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → ⊥)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂) → ¬ 𝛾₃)
Theorem	rcp-FALSENEGI4 436	'¬' Introduction with '⊥'. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → ⊥)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → ¬ 𝛾₄)
Theorem	rcp-FALSENEGI5 437	'¬' Introduction with '⊥'. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → ⊥)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → ¬ 𝛾₅)
5.2  Logical Equivalencies.
5.2.1  Identity Laws for Conjunction and Disjunction.
Theorem	idandtruel-P4.19a 438	'∧' Identity is '⊤' (left). †
⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)
Theorem	idandtruer-P4.19b 439	'∧' Identity is '⊤' (right). †
⊢ ((𝜑 ∧ ⊤) ↔ 𝜑)
Theorem	idorfalsel-P4.20a 440	'∨' Identity is '⊥' (left). †
⊢ ((⊥ ∨ 𝜑) ↔ 𝜑)
Theorem	idorfalser-P4.20b 441	'∨' Identity is '⊥' (right). †
⊢ ((𝜑 ∨ ⊥) ↔ 𝜑)
5.2.2  More Equivalence Laws Involving "True" and "False".
Theorem	thmeqtrue-P4.21a 442	Any Theorem is Logically Equivalent to '⊤'. †
⊢ 𝜑    ⇒   ⊢ (𝜑 ↔ ⊤)
Theorem	nthmeqfalse-P4.21b 443	Any Refuted Statement is Logically Equivalent to '⊥'. †
⊢ ¬ 𝜑    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	trueie-P4.22a 444	'⊤' Introduction and Elimination (closed form). †
⊢ ((⊤ → 𝜑) ↔ 𝜑)
Theorem	falseie-P4.22b 445	'⊥' Introduction and Elimination (closed form). †
⊢ ((𝜑 → ⊥) ↔ ¬ 𝜑)
5.2.3  Identity Laws Involving Theorems.
Theorem	idandthml-P4.23a 446	'∧' Identity is Any Theorem (left). †
⊢ 𝜑    ⇒   ⊢ ((𝜑 ∧ 𝜓) ↔ 𝜓)
Theorem	idandthmr-P4.23b 447	'∧' Identity is Any Theorem (right). †
⊢ 𝜑    ⇒   ⊢ ((𝜓 ∧ 𝜑) ↔ 𝜓)
Theorem	idornthml-P4.24a 448	'∨' Identity is Any Refuted Statement (left). †
⊢ ¬ 𝜑    ⇒   ⊢ ((𝜑 ∨ 𝜓) ↔ 𝜓)
Theorem	idornthmr-P4.24b 449	'∨' Identity is Any Refuted Statement (right). †
⊢ ¬ 𝜑    ⇒   ⊢ ((𝜓 ∨ 𝜑) ↔ 𝜓)
5.2.4  Idempotency Laws.
Theorem	idempotand-P4.25a 450	Idempotency Law for '∧'. †
⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)
Theorem	idempotor-P4.25b 451	Idempotency Law for '∨'. †
⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)
5.2.5  De Morgan's Laws.
5.2.5.1  Parts of De Morgan's Laws.
Theorem	dmorgafwd-L4.1 452	De Morgan's Law A: Forward Implication Lemma. †
⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
Theorem	dmorgarev-L4.2 453	De Morgan's Law A: Reverse Implication Lemma. †
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
Theorem	dmorgbfwd-L4.3 454	De Morgan's Law B: Forward Implication Lemma.
⊢ (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	dmorgbrev-L4.4 455	De Morgan's Law B: Reverse Implication Lemma. †
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
5.2.5.2  De Morgan's Laws.
Theorem	dmorga-P4.26a 456	De Morgan's Law A. †
⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
Theorem	dmorgb-P4.26b 457	De Morgan's Law B.
⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	dmorgbint-P4.26c 458	De Morgan's Law B ( Intuitionist Version ). † The reverse of this implication cannot be deduced in an intuitionist framework. However, it can be added as an axiom to create an intermediate strength logic.
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
5.2.6  Distributive Laws.
5.2.6.1  Conjunction and Disjunction.
Theorem	andoveror-P4.27-L1 459	Lemma for andoveror-P4.27a 461. † [Auxiliary lemma - not displayed.]
Theorem	andoveror-P4.27-L2 460	Lemma for andoveror-P4.27a 461. † [Auxiliary lemma - not displayed.]
Theorem	andoveror-P4.27a 461	'∧' Distributes Over '∨' . †
⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
Theorem	oroverand-P4.27-L3 462	Lemma for oroverand-P4.27b 464. † [Auxiliary lemma - not displayed.]
Theorem	oroverand-P4.27-L4 463	Lemma for oroverand-P4.27b 464. † [Auxiliary lemma - not displayed.]
Theorem	oroverand-P4.27b 464	'∨' Distributes Over '∧'. †
⊢ ((𝜑 ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒)))
Theorem	oroverim-P4.28-L1 465	Lemma for oroverim-P4.28a 467 and oroverimint-P4.28c 470. † [Auxiliary lemma - not displayed.]
Theorem	oroverim-P4.28-L2 466	Lemma for oroverim-P4.28a 467. [Auxiliary lemma - not displayed.]
Theorem	oroverim-P4.28a 467	'∨' Distributes Over '→'.
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) ↔ ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)))
Theorem	oroverbi-P4.28-L3 468	Lemma for oroverbi-P4.28b 469 and oroverbiint-P4.28d 471. † [Auxiliary lemma - not displayed.]
Theorem	oroverbi-P4.28b 469	'∨' Distributes Over '↔'.
⊢ ((𝜑 ∨ (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ 𝜒)))
Theorem	oroverimint-P4.28c 470	One Direction of '∨' Distributes Over '→'. † Only this version is derivalbe with intuitionist logic.
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)))
Theorem	oroverbiint-P4.28d 471	One Direction of '∨' Distributes Over '↔'. † Only this version is deducible with intuitionist logic.
⊢ ((𝜑 ∨ (𝜓 ↔ 𝜒)) → ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ 𝜒)))
5.2.6.2  Left Implication.
Theorem	imoverand-P4.29a 472	'→' Left Distributes Over '∧'. †
⊢ ((𝜑 → (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)))
Theorem	imoveror-P4.29-L1 473	Lemma for imoveror-P4.29b 474 and imoverorint-P4.29c 475. † [Auxiliary lemma - not displayed.]
Theorem	imoveror-P4.29b 474	'→' Left Distributes Over '∨' .
⊢ ((𝜑 → (𝜓 ∨ 𝜒)) ↔ ((𝜑 → 𝜓) ∨ (𝜑 → 𝜒)))
Theorem	imoverorint-P4.29c 475	One Direction of '→' Left Distributes Over '∨' . † Only this direction is deducible with intuitionist logic.
⊢ (((𝜑 → 𝜓) ∨ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ∨ 𝜒)))
Theorem	imoverim-P4.30-L1 476	Lemma for imoverim-P4.30a . † [Auxiliary lemma - not displayed.]
Theorem	imoverim-P4.30a 477	'→' Distributes Over Itself . †
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	imoverbi-P4.30-L2 478	Lemma for imoverbi-P4.30b 479. † [Auxiliary lemma - not displayed.]
Theorem	imoverbi-P4.30b 479	'→' Left Distributes Over '↔'. †
⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)))
5.2.7  Antidistributive Laws.
Theorem	rimoverand-P4.31-L1 480	Lemma for rimoverand-P4.31a 481 and rimoverandint-P4.31c 483. † [Auxiliary lemma - not displayed.]
Theorem	rimoverand-P4.31a 481	'→' is Antidistributive on the Right Over '∧'.
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜒) ∨ (𝜓 → 𝜒)))
Theorem	rimoveror-P4.31b 482	'→' is Antidistributive on the Right Over '∨' . †
⊢ (((𝜑 ∨ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜒) ∧ (𝜓 → 𝜒)))
Theorem	rimoverandint-P4.31c 483	One Direction of '→' is Antidistributive on the Right Over '∧' . † Only this direction is deducible with intuitionist logic.
⊢ (((𝜑 → 𝜒) ∨ (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒))
5.2.8  More Useful Logical Equivalencies.
Theorem	lemma-L4.5 484	Lemma 4.5.
⊢ (¬ (𝜑 ∧ ¬ 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))
Theorem	imasor-P4.32-L1 485	Lemma for imasor-P4.32a 487. [Auxiliary lemma - not displayed.]
Theorem	imasor-P4.32-L2 486	Lemma for imasor-P4.32a 487 and imasorint-P4.32b 488. † [Auxiliary lemma - not displayed.]
Theorem	imasor-P4.32a 487	'→' in Terms of '∨'.
⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))
Theorem	imasorint-P4.32b 488	One Direction of '→' in Terms of '∨'. † Only this direction is deducible with intuitionist logic.
⊢ ((¬ 𝜑 ∨ 𝜓) → (𝜑 → 𝜓))
Theorem	imasand-P4.33a 489	'→' in Terms of '∧'.
⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
Theorem	imasandint-P4.33b 490	One Direction of '→' in Terms of '∧'. † Only this direction is deducible with intuitionist logic.
⊢ ((𝜑 → 𝜓) → ¬ (𝜑 ∧ ¬ 𝜓))
Theorem	biasandor-P4.34a 491	'↔' in Terms of '∧' and '∨'.
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)))
Theorem	biasandorint-P4.34b 492	One direction of '↔' in Terms of '∧' and '∨'. † Only this direction is deducible with intuitionist logic.
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) → (𝜑 ↔ 𝜓))
5.2.9  Truth Tables.
5.2.9.1  Negation.
Theorem	truthtblnegt-P4.35a 493	¬ T ⇔ F. †
⊢ (¬ ⊤ ↔ ⊥)
Theorem	truthtblnegf-P4.35b 494	¬ F ⇔ T. †
⊢ (¬ ⊥ ↔ ⊤)
5.2.9.2  Implication.
Theorem	truthtbltimt-P4.36a 495	( T → T ) ⇔ T. †
⊢ ((⊤ → ⊤) ↔ ⊤)
Theorem	truthtbltimf-P4.36b 496	( T → F ) ⇔ F. †
⊢ ((⊤ → ⊥) ↔ ⊥)
Theorem	truthtblfimt-P4.36c 497	( F → T ) ⇔ T. †
⊢ ((⊥ → ⊤) ↔ ⊤)
Theorem	truthtblfimf-P4.36d 498	( F → F ) ⇔ T. †
⊢ ((⊥ → ⊥) ↔ ⊤)
5.2.9.3  Conjunction.
Theorem	truthtbltandt-P4.37a 499	( T ∧ T ) ⇔ T. †
⊢ ((⊤ ∧ ⊤) ↔ ⊤)
Theorem	truthtbltandf-P4.37b 500	( T ∧ F ) ⇔ F. †
⊢ ((⊤ ∧ ⊥) ↔ ⊥)