Home | Intuitionistic Logic Explorer Theorem List (p. 9 of 114) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | con34bdc 801 | Contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116, but for a decidable proposition. (Contributed by Jim Kingdon, 24-Apr-2018.) |
⊢ (DECID 𝜓 → ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))) | ||
Theorem | notnotbdc 802 | Double negation equivalence for a decidable proposition. Like Theorem *4.13 of [WhiteheadRussell] p. 117, but with a decidability antecendent. The forward direction, notnot 592, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 13-Mar-2018.) |
⊢ (DECID 𝜑 → (𝜑 ↔ ¬ ¬ 𝜑)) | ||
Theorem | con1biimdc 803 | Contraposition. (Contributed by Jim Kingdon, 4-Apr-2018.) |
⊢ (DECID 𝜑 → ((¬ 𝜑 ↔ 𝜓) → (¬ 𝜓 ↔ 𝜑))) | ||
Theorem | con1bidc 804 | Contraposition. (Contributed by Jim Kingdon, 17-Apr-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → ((¬ 𝜑 ↔ 𝜓) ↔ (¬ 𝜓 ↔ 𝜑)))) | ||
Theorem | con2bidc 805 | Contraposition. (Contributed by Jim Kingdon, 17-Apr-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜑)))) | ||
Theorem | con1biddc 806 | A contraposition deduction. (Contributed by Jim Kingdon, 4-Apr-2018.) |
⊢ (𝜑 → (DECID 𝜓 → (¬ 𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (¬ 𝜒 ↔ 𝜓))) | ||
Theorem | con1biidc 807 | A contraposition inference. (Contributed by Jim Kingdon, 15-Mar-2018.) |
⊢ (DECID 𝜑 → (¬ 𝜑 ↔ 𝜓)) ⇒ ⊢ (DECID 𝜑 → (¬ 𝜓 ↔ 𝜑)) | ||
Theorem | con1bdc 808 | Contraposition. Bidirectional version of con1dc 789. (Contributed by NM, 5-Aug-1993.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → ((¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → 𝜑)))) | ||
Theorem | con2biidc 809 | A contraposition inference. (Contributed by Jim Kingdon, 15-Mar-2018.) |
⊢ (DECID 𝜓 → (𝜑 ↔ ¬ 𝜓)) ⇒ ⊢ (DECID 𝜓 → (𝜓 ↔ ¬ 𝜑)) | ||
Theorem | con2biddc 810 | A contraposition deduction. (Contributed by Jim Kingdon, 11-Apr-2018.) |
⊢ (𝜑 → (DECID 𝜒 → (𝜓 ↔ ¬ 𝜒))) ⇒ ⊢ (𝜑 → (DECID 𝜒 → (𝜒 ↔ ¬ 𝜓))) | ||
Theorem | condandc 811 | Proof by contradiction. This only holds for decidable propositions, as it is part of the family of theorems which assume ¬ 𝜓, derive a contradiction, and therefore conclude 𝜓. By contrast, assuming 𝜓, deriving a contradiction, and therefore concluding ¬ 𝜓, as in pm2.65 618, is valid for all propositions. (Contributed by Jim Kingdon, 13-May-2018.) |
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ 𝜒) ⇒ ⊢ (DECID 𝜓 → (𝜑 → 𝜓)) | ||
Theorem | bijadc 812 | Combine antecedents into a single biconditional. This inference is reminiscent of jadc 796. (Contributed by Jim Kingdon, 4-May-2018.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ (DECID 𝜓 → ((𝜑 ↔ 𝜓) → 𝜒)) | ||
Theorem | pm5.18dc 813 | Relationship between an equivalence and an equivalence with some negation, for decidable propositions. Based on theorem *5.18 of [WhiteheadRussell] p. 124. Given decidability, we can consider ¬ (𝜑 ↔ ¬ 𝜓) to represent "negated exclusive-or". (Contributed by Jim Kingdon, 4-Apr-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ↔ ¬ 𝜓)))) | ||
Theorem | dfandc 814 | Definition of 'and' in terms of negation and implication, for decidable propositions. The forward direction holds for all propositions, and can (basically) be found at pm3.2im 599. (Contributed by Jim Kingdon, 30-Apr-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)))) | ||
Theorem | pm2.13dc 815 | A decidable proposition or its triple negation is true. Theorem *2.13 of [WhiteheadRussell] p. 101 with decidability condition added. (Contributed by Jim Kingdon, 13-May-2018.) |
⊢ (DECID 𝜑 → (𝜑 ∨ ¬ ¬ ¬ 𝜑)) | ||
Theorem | pm4.63dc 816 | Theorem *4.63 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 1-May-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (𝜑 → ¬ 𝜓) ↔ (𝜑 ∧ 𝜓)))) | ||
Theorem | pm4.67dc 817 | Theorem *4.67 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 1-May-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (¬ 𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∧ 𝜓)))) | ||
Theorem | annimim 818 | Express conjunction in terms of implication. One direction of Theorem *4.61 of [WhiteheadRussell] p. 120. The converse holds for decidable propositions, as can be seen at annimdc 881. (Contributed by Jim Kingdon, 24-Dec-2017.) |
⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 → 𝜓)) | ||
Theorem | pm4.65r 819 | One direction of Theorem *4.65 of [WhiteheadRussell] p. 120. The converse holds in classical logic. (Contributed by Jim Kingdon, 28-Jul-2018.) |
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (¬ 𝜑 → 𝜓)) | ||
Theorem | dcim 820 | An implication between two decidable propositions is decidable. (Contributed by Jim Kingdon, 28-Mar-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 → 𝜓))) | ||
Theorem | imanim 821 | Express implication in terms of conjunction. The converse only holds given a decidability condition; see imandc 822. (Contributed by Jim Kingdon, 24-Dec-2017.) |
⊢ ((𝜑 → 𝜓) → ¬ (𝜑 ∧ ¬ 𝜓)) | ||
Theorem | imandc 822 | Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176, with an added decidability condition. The forward direction, imanim 821, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 25-Apr-2018.) |
⊢ (DECID 𝜓 → ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))) | ||
Theorem | pm4.14dc 823 | Theorem *4.14 of [WhiteheadRussell] p. 117, given a decidability condition. (Contributed by Jim Kingdon, 24-Apr-2018.) |
⊢ (DECID 𝜒 → (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓))) | ||
Theorem | pm3.37 824 | Theorem *3.37 (Transp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ∧ 𝜓) → 𝜒) → ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)) | ||
Theorem | pm4.15 825 | Theorem *4.15 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 18-Nov-2012.) |
⊢ (((𝜑 ∧ 𝜓) → ¬ 𝜒) ↔ ((𝜓 ∧ 𝜒) → ¬ 𝜑)) | ||
Theorem | pm2.54dc 826 | Deriving disjunction from implication for a decidable proposition. Based on theorem *2.54 of [WhiteheadRussell] p. 107. The converse, pm2.53 674, holds whether the proposition is decidable or not. (Contributed by Jim Kingdon, 26-Mar-2018.) |
⊢ (DECID 𝜑 → ((¬ 𝜑 → 𝜓) → (𝜑 ∨ 𝜓))) | ||
Theorem | dfordc 827 | Definition of 'or' in terms of negation and implication for a decidable proposition. Based on definition of [Margaris] p. 49. One direction, pm2.53 674, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 26-Mar-2018.) |
⊢ (DECID 𝜑 → ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))) | ||
Theorem | pm2.25dc 828 | Elimination of disjunction based on a disjunction, for a decidable proposition. Based on theorem *2.25 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
⊢ (DECID 𝜑 → (𝜑 ∨ ((𝜑 ∨ 𝜓) → 𝜓))) | ||
Theorem | pm2.68dc 829 | Concluding disjunction from implication for a decidable proposition. Based on theorem *2.68 of [WhiteheadRussell] p. 108. Converse of pm2.62 700 and one half of dfor2dc 830. (Contributed by Jim Kingdon, 27-Mar-2018.) |
⊢ (DECID 𝜑 → (((𝜑 → 𝜓) → 𝜓) → (𝜑 ∨ 𝜓))) | ||
Theorem | dfor2dc 830 | Logical 'or' expressed in terms of implication only, for a decidable proposition. Based on theorem *5.25 of [WhiteheadRussell] p. 124. (Contributed by Jim Kingdon, 27-Mar-2018.) |
⊢ (DECID 𝜑 → ((𝜑 ∨ 𝜓) ↔ ((𝜑 → 𝜓) → 𝜓))) | ||
Theorem | imimorbdc 831 | Simplify an implication between implications, for a decidable proposition. (Contributed by Jim Kingdon, 18-Mar-2018.) |
⊢ (DECID 𝜓 → (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∨ 𝜒)))) | ||
Theorem | imordc 832 | Implication in terms of disjunction for a decidable proposition. Based on theorem *4.6 of [WhiteheadRussell] p. 120. The reverse direction, imorr 833, holds for all propositions. (Contributed by Jim Kingdon, 20-Apr-2018.) |
⊢ (DECID 𝜑 → ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))) | ||
Theorem | imorr 833 | Implication in terms of disjunction. One direction of theorem *4.6 of [WhiteheadRussell] p. 120. The converse holds for decidable propositions, as seen at imordc 832. (Contributed by Jim Kingdon, 21-Jul-2018.) |
⊢ ((¬ 𝜑 ∨ 𝜓) → (𝜑 → 𝜓)) | ||
Theorem | pm4.62dc 834 | Implication in terms of disjunction. Like Theorem *4.62 of [WhiteheadRussell] p. 120, but for a decidable antecedent. (Contributed by Jim Kingdon, 21-Apr-2018.) |
⊢ (DECID 𝜑 → ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))) | ||
Theorem | ianordc 835 | Negated conjunction in terms of disjunction (DeMorgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120, but where one proposition is decidable. The reverse direction, pm3.14 703, holds for all propositions, but the equivalence only holds where one proposition is decidable. (Contributed by Jim Kingdon, 21-Apr-2018.) |
⊢ (DECID 𝜑 → (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))) | ||
Theorem | oibabs 836 | Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.) |
⊢ (((𝜑 ∨ 𝜓) → (𝜑 ↔ 𝜓)) ↔ (𝜑 ↔ 𝜓)) | ||
Theorem | pm4.64dc 837 | Theorem *4.64 of [WhiteheadRussell] p. 120, given a decidability condition. The reverse direction, pm2.53 674, holds for all propositions. (Contributed by Jim Kingdon, 2-May-2018.) |
⊢ (DECID 𝜑 → ((¬ 𝜑 → 𝜓) ↔ (𝜑 ∨ 𝜓))) | ||
Theorem | pm4.66dc 838 | Theorem *4.66 of [WhiteheadRussell] p. 120, given a decidability condition. (Contributed by Jim Kingdon, 2-May-2018.) |
⊢ (DECID 𝜑 → ((¬ 𝜑 → ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))) | ||
Theorem | pm4.52im 839 | One direction of theorem *4.52 of [WhiteheadRussell] p. 120. The converse also holds in classical logic. (Contributed by Jim Kingdon, 27-Jul-2018.) |
⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ (¬ 𝜑 ∨ 𝜓)) | ||
Theorem | pm4.53r 840 | One direction of theorem *4.53 of [WhiteheadRussell] p. 120. The converse also holds in classical logic. (Contributed by Jim Kingdon, 27-Jul-2018.) |
⊢ ((¬ 𝜑 ∨ 𝜓) → ¬ (𝜑 ∧ ¬ 𝜓)) | ||
Theorem | pm4.54dc 841 | Theorem *4.54 of [WhiteheadRussell] p. 120, for decidable propositions. One form of DeMorgan's law. (Contributed by Jim Kingdon, 2-May-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → ((¬ 𝜑 ∧ 𝜓) ↔ ¬ (𝜑 ∨ ¬ 𝜓)))) | ||
Theorem | pm4.56 842 | Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓)) | ||
Theorem | oranim 843 | Disjunction in terms of conjunction (DeMorgan's law). One direction of Theorem *4.57 of [WhiteheadRussell] p. 120. The converse does not hold intuitionistically but does hold in classical logic. (Contributed by Jim Kingdon, 25-Jul-2018.) |
⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓)) | ||
Theorem | pm4.78i 844 | Implication distributes over disjunction. One direction of Theorem *4.78 of [WhiteheadRussell] p. 121. The converse holds in classical logic. (Contributed by Jim Kingdon, 15-Jan-2018.) |
⊢ (((𝜑 → 𝜓) ∨ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ∨ 𝜒))) | ||
Theorem | pm4.79dc 845 | Equivalence between a disjunction of two implications, and a conjunction and an implication. Based on theorem *4.79 of [WhiteheadRussell] p. 121 but with additional decidability antecedents. (Contributed by Jim Kingdon, 28-Mar-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → (((𝜓 → 𝜑) ∨ (𝜒 → 𝜑)) ↔ ((𝜓 ∧ 𝜒) → 𝜑)))) | ||
Theorem | pm5.17dc 846 | Two ways of stating exclusive-or which are equivalent for a decidable proposition. Based on theorem *5.17 of [WhiteheadRussell] p. 124. (Contributed by Jim Kingdon, 16-Apr-2018.) |
⊢ (DECID 𝜓 → (((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) ↔ (𝜑 ↔ ¬ 𝜓))) | ||
Theorem | pm2.85dc 847 | Reverse distribution of disjunction over implication, given decidability. Based on theorem *2.85 of [WhiteheadRussell] p. 108. (Contributed by Jim Kingdon, 1-Apr-2018.) |
⊢ (DECID 𝜑 → (((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)) → (𝜑 ∨ (𝜓 → 𝜒)))) | ||
Theorem | orimdidc 848 | Disjunction distributes over implication. The forward direction, pm2.76 755, is valid intuitionistically. The reverse direction holds if 𝜑 is decidable, as can be seen at pm2.85dc 847. (Contributed by Jim Kingdon, 1-Apr-2018.) |
⊢ (DECID 𝜑 → ((𝜑 ∨ (𝜓 → 𝜒)) ↔ ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)))) | ||
Theorem | pm2.26dc 849 | Decidable proposition version of theorem *2.26 of [WhiteheadRussell] p. 104. (Contributed by Jim Kingdon, 20-Apr-2018.) |
⊢ (DECID 𝜑 → (¬ 𝜑 ∨ ((𝜑 → 𝜓) → 𝜓))) | ||
Theorem | pm4.81dc 850 | Theorem *4.81 of [WhiteheadRussell] p. 122, for decidable propositions. This one needs a decidability condition, but compare with pm4.8 656 which holds for all propositions. (Contributed by Jim Kingdon, 4-Jul-2018.) |
⊢ (DECID 𝜑 → ((¬ 𝜑 → 𝜑) ↔ 𝜑)) | ||
Theorem | pm5.11dc 851 | A decidable proposition or its negation implies a second proposition. Based on theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 29-Mar-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 → 𝜓) ∨ (¬ 𝜑 → 𝜓)))) | ||
Theorem | pm5.12dc 852 | Excluded middle with antecedents for a decidable consequent. Based on theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 30-Mar-2018.) |
⊢ (DECID 𝜓 → ((𝜑 → 𝜓) ∨ (𝜑 → ¬ 𝜓))) | ||
Theorem | pm5.14dc 853 | A decidable proposition is implied by or implies other propositions. Based on theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 30-Mar-2018.) |
⊢ (DECID 𝜓 → ((𝜑 → 𝜓) ∨ (𝜓 → 𝜒))) | ||
Theorem | pm5.13dc 854 | An implication holds in at least one direction, where one proposition is decidable. Based on theorem *5.13 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 30-Mar-2018.) |
⊢ (DECID 𝜓 → ((𝜑 → 𝜓) ∨ (𝜓 → 𝜑))) | ||
Theorem | pm5.55dc 855 | A disjunction is equivalent to one of its disjuncts, given a decidable disjunct. Based on theorem *5.55 of [WhiteheadRussell] p. 125. (Contributed by Jim Kingdon, 30-Mar-2018.) |
⊢ (DECID 𝜑 → (((𝜑 ∨ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∨ 𝜓) ↔ 𝜓))) | ||
Theorem | peircedc 856 | Peirce's theorem for a decidable proposition. This odd-looking theorem can be seen as an alternative to exmiddc 780, condc 785, or notnotrdc 787 in the sense of expressing the "difference" between an intuitionistic system of propositional calculus and a classical system. In intuitionistic logic, it only holds for decidable propositions. (Contributed by Jim Kingdon, 3-Jul-2018.) |
⊢ (DECID 𝜑 → (((𝜑 → 𝜓) → 𝜑) → 𝜑)) | ||
Theorem | looinvdc 857 | The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz, but where one of the propositions is decidable. Using dfor2dc 830, we can see that this expresses "disjunction commutes." Theorem *2.69 of [WhiteheadRussell] p. 108 (plus the decidability condition). (Contributed by NM, 12-Aug-2004.) |
⊢ (DECID 𝜑 → (((𝜑 → 𝜓) → 𝜓) → ((𝜓 → 𝜑) → 𝜑))) | ||
Theorem | dftest 858 |
A proposition is testable iff its negative or double-negative is true.
See Chapter 2 [Moschovakis] p. 2.
Our notation for testability is DECID ¬ before the formula in question. For example, DECID ¬ 𝑥 = 𝑦 corresponds to "x = y is testable". (Contributed by David A. Wheeler, 13-Aug-2018.) |
⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑)) | ||
Theorem | testbitestn 859 | A proposition is testable iff its negation is testable. See also dcn 782 (which could be read as "Decidability implies testability"). (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ (DECID ¬ 𝜑 ↔ DECID ¬ ¬ 𝜑) | ||
Theorem | stabtestimpdc 860 | "Stable and testable" is equivalent to decidable. (Contributed by David A. Wheeler, 13-Aug-2018.) |
⊢ ((STAB 𝜑 ∧ DECID ¬ 𝜑) ↔ DECID 𝜑) | ||
Theorem | pm5.21nd 861 | Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜃) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) & ⊢ (𝜃 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | pm5.35 862 | Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ↔ 𝜒))) | ||
Theorem | pm5.54dc 863 | A conjunction is equivalent to one of its conjuncts, given a decidable conjunct. Based on theorem *5.54 of [WhiteheadRussell] p. 125. (Contributed by Jim Kingdon, 30-Mar-2018.) |
⊢ (DECID 𝜑 → (((𝜑 ∧ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∧ 𝜓) ↔ 𝜓))) | ||
Theorem | baib 864 | Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜑 ↔ 𝜒)) | ||
Theorem | baibr 865 | Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜒 ↔ 𝜑)) | ||
Theorem | rbaib 866 | Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜒 → (𝜑 ↔ 𝜓)) | ||
Theorem | rbaibr 867 | Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜒 → (𝜓 ↔ 𝜑)) | ||
Theorem | baibd 868 | Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃)) | ||
Theorem | rbaibd 869 | Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒)) | ||
Theorem | pm5.44 870 | Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) → ((𝜑 → 𝜒) ↔ (𝜑 → (𝜓 ∧ 𝜒)))) | ||
Theorem | pm5.6dc 871 | Conjunction in antecedent versus disjunction in consequent, for a decidable proposition. Theorem *5.6 of [WhiteheadRussell] p. 125, with decidability condition added. The reverse implication holds for all propositions (see pm5.6r 872). (Contributed by Jim Kingdon, 2-Apr-2018.) |
⊢ (DECID 𝜓 → (((𝜑 ∧ ¬ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 ∨ 𝜒)))) | ||
Theorem | pm5.6r 872 | Conjunction in antecedent versus disjunction in consequent. One direction of Theorem *5.6 of [WhiteheadRussell] p. 125. If 𝜓 is decidable, the converse also holds (see pm5.6dc 871). (Contributed by Jim Kingdon, 4-Aug-2018.) |
⊢ ((𝜑 → (𝜓 ∨ 𝜒)) → ((𝜑 ∧ ¬ 𝜓) → 𝜒)) | ||
Theorem | orcanai 873 | Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.) |
⊢ (𝜑 → (𝜓 ∨ 𝜒)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) | ||
Theorem | intnan 874 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.) |
⊢ ¬ 𝜑 ⇒ ⊢ ¬ (𝜓 ∧ 𝜑) | ||
Theorem | intnanr 875 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.) |
⊢ ¬ 𝜑 ⇒ ⊢ ¬ (𝜑 ∧ 𝜓) | ||
Theorem | intnand 876 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓)) | ||
Theorem | intnanrd 877 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) | ||
Theorem | dcan 878 | A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∧ 𝜓))) | ||
Theorem | dcor 879 | A disjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 21-Apr-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓))) | ||
Theorem | dcbi 880 | An equivalence of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ↔ 𝜓))) | ||
Theorem | annimdc 881 | Express conjunction in terms of implication. The forward direction, annimim 818, is valid for all propositions, but as an equivalence, it requires a decidability condition. (Contributed by Jim Kingdon, 25-Apr-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)))) | ||
Theorem | pm4.55dc 882 | Theorem *4.55 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 2-May-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (¬ 𝜑 ∧ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓)))) | ||
Theorem | orandc 883 | Disjunction in terms of conjunction (De Morgan's law), for decidable propositions. Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by Jim Kingdon, 13-Dec-2021.) |
⊢ ((DECID 𝜑 ∧ DECID 𝜓) → ((𝜑 ∨ 𝜓) ↔ ¬ (¬ 𝜑 ∧ ¬ 𝜓))) | ||
Theorem | mpbiran 884 | Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.) (Revised by NM, 9-Jan-2015.) |
⊢ 𝜓 & ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜒) | ||
Theorem | mpbiran2 885 | Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) (Revised by NM, 9-Jan-2015.) |
⊢ 𝜒 & ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
Theorem | mpbir2an 886 | Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) (Revised by NM, 9-Jan-2015.) |
⊢ 𝜓 & ⊢ 𝜒 & ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ 𝜑 | ||
Theorem | mpbi2and 887 | Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | mpbir2and 888 | Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm5.62dc 889 | Theorem *5.62 of [WhiteheadRussell] p. 125, for a decidable proposition. (Contributed by Jim Kingdon, 12-May-2018.) |
⊢ (DECID 𝜓 → (((𝜑 ∧ 𝜓) ∨ ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))) | ||
Theorem | pm5.63dc 890 | Theorem *5.63 of [WhiteheadRussell] p. 125, for a decidable proposition. (Contributed by Jim Kingdon, 12-May-2018.) |
⊢ (DECID 𝜑 → ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ (¬ 𝜑 ∧ 𝜓)))) | ||
Theorem | bianfi 891 | A wff conjoined with falsehood is false. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.) |
⊢ ¬ 𝜑 ⇒ ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑)) | ||
Theorem | bianfd 892 | A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | pm4.43 893 | Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.) |
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ ¬ 𝜓))) | ||
Theorem | pm4.82 894 | Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ↔ ¬ 𝜑) | ||
Theorem | pm4.83dc 895 | Theorem *4.83 of [WhiteheadRussell] p. 122, for decidable propositions. As with other case elimination theorems, like pm2.61dc 798, it only holds for decidable propositions. (Contributed by Jim Kingdon, 12-May-2018.) |
⊢ (DECID 𝜑 → (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜓)) ↔ 𝜓)) | ||
Theorem | biantr 896 | A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 18-Aug-1993.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜓)) → (𝜑 ↔ 𝜒)) | ||
Theorem | orbididc 897 | Disjunction distributes over the biconditional, for a decidable proposition. Based on an axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.3384. (Contributed by Jim Kingdon, 2-Apr-2018.) |
⊢ (DECID 𝜑 → ((𝜑 ∨ (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ 𝜒)))) | ||
Theorem | pm5.7dc 898 | Disjunction distributes over the biconditional, for a decidable proposition. Based on theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbididc 897. (Contributed by Jim Kingdon, 2-Apr-2018.) |
⊢ (DECID 𝜒 → (((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) ↔ (𝜒 ∨ (𝜑 ↔ 𝜓)))) | ||
Theorem | bigolden 899 | Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.) |
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓))) | ||
Theorem | anordc 900 | Conjunction in terms of disjunction (DeMorgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120, but where the propositions are decidable. The forward direction, pm3.1 704, holds for all propositions, but the equivalence only holds given decidability. (Contributed by Jim Kingdon, 21-Apr-2018.) |
⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ 𝜓) ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |