![]() |
Metamath
Proof Explorer Theorem List (p. 10 of 435) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28329) |
![]() (28330-29854) |
![]() (29855-43446) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | olc 901 | Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.) |
⊢ (𝜑 → (𝜓 ∨ 𝜑)) | ||
Theorem | pm1.4 902 | Axiom *1.4 of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑)) | ||
Theorem | orcom 903 | Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 15-Nov-2012.) |
⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑)) | ||
Theorem | orcomd 904 | Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.) |
⊢ (𝜑 → (𝜓 ∨ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 ∨ 𝜓)) | ||
Theorem | orcoms 905 | Commutation of disjuncts in antecedent. (Contributed by NM, 2-Dec-2012.) |
⊢ ((𝜑 ∨ 𝜓) → 𝜒) ⇒ ⊢ ((𝜓 ∨ 𝜑) → 𝜒) | ||
Theorem | orcd 906 | Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 27817. (Contributed by NM, 20-Sep-2007.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ∨ 𝜒)) | ||
Theorem | olcd 907 | Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 27817. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜒 ∨ 𝜓)) | ||
Theorem | orcs 908 | Deduction eliminating disjunct. Notational convention: We sometimes suffix with "s" the label of an inference that manipulates an antecedent, leaving the consequent unchanged. The "s" means that the inference eliminates the need for a syllogism (syl 17) -type inference in a proof. (Contributed by NM, 21-Jun-1994.) |
⊢ ((𝜑 ∨ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | olcs 909 | Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.) (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
⊢ ((𝜑 ∨ 𝜓) → 𝜒) ⇒ ⊢ (𝜓 → 𝜒) | ||
Theorem | mtord 910 | A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.) |
⊢ (𝜑 → ¬ 𝜒) & ⊢ (𝜑 → ¬ 𝜃) & ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | pm3.2ni 911 | Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.) |
⊢ ¬ 𝜑 & ⊢ ¬ 𝜓 ⇒ ⊢ ¬ (𝜑 ∨ 𝜓) | ||
Theorem | pm2.45 912 | Theorem *2.45 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑) | ||
Theorem | pm2.46 913 | Theorem *2.46 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓) | ||
Theorem | pm2.47 914 | Theorem *2.47 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∨ 𝜓)) | ||
Theorem | pm2.48 915 | Theorem *2.48 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 ∨ 𝜓) → (𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm2.49 916 | Theorem *2.49 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓)) | ||
Theorem | norbi 917 | If neither of two propositions is true, then these propositions are equivalent. (Contributed by BJ, 26-Apr-2019.) |
⊢ (¬ (𝜑 ∨ 𝜓) → (𝜑 ↔ 𝜓)) | ||
Theorem | nbior 918 | If two propositions are not equivalent, then at least one is true. (Contributed by BJ, 19-Apr-2019.) (Proof shortened by Wolf Lammen, 19-Jan-2020.) |
⊢ (¬ (𝜑 ↔ 𝜓) → (𝜑 ∨ 𝜓)) | ||
Theorem | orel1 919 | Elimination of disjunction by denial of a disjunct. Theorem *2.55 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 21-Jul-2012.) |
⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓)) | ||
Theorem | pm2.25 920 | Theorem *2.25 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 ∨ ((𝜑 ∨ 𝜓) → 𝜓)) | ||
Theorem | orel2 921 | Elimination of disjunction by denial of a disjunct. Theorem *2.56 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 5-Apr-2013.) |
⊢ (¬ 𝜑 → ((𝜓 ∨ 𝜑) → 𝜓)) | ||
Theorem | pm2.67-2 922 | Slight generalization of Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ∨ 𝜒) → 𝜓) → (𝜑 → 𝜓)) | ||
Theorem | pm2.67 923 | Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ∨ 𝜓) → 𝜓) → (𝜑 → 𝜓)) | ||
Theorem | curryax 924 | A non-intuitionistic positive statement, sometimes called a paradox of material implication. Sometimes called Curry's axiom. Similar to exmid 925 but positive. For another non-intuitionistic positive statement, see peirce 194. (Contributed by BJ, 4-Apr-2021.) |
⊢ (𝜑 ∨ (𝜑 → 𝜓)) | ||
Theorem | exmid 925 | Law of excluded middle, also called the principle of tertium non datur. 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. In intuitionistic logic, if this statement is true for some 𝜑, then 𝜑 is decidable. (Contributed by NM, 29-Dec-1992.) |
⊢ (𝜑 ∨ ¬ 𝜑) | ||
Theorem | exmidd 926 | Law of excluded middle in a context. (Contributed by Mario Carneiro, 9-Feb-2017.) |
⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓)) | ||
Theorem | pm2.1 927 | Theorem *2.1 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) |
⊢ (¬ 𝜑 ∨ 𝜑) | ||
Theorem | pm2.13 928 | Theorem *2.13 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 ∨ ¬ ¬ ¬ 𝜑) | ||
Theorem | pm2.621 929 | Theorem *2.621 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) → ((𝜑 ∨ 𝜓) → 𝜓)) | ||
Theorem | pm2.62 930 | Theorem *2.62 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Dec-2013.) |
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 → 𝜓) → 𝜓)) | ||
Theorem | pm2.68 931 | Theorem *2.68 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) → 𝜓) → (𝜑 ∨ 𝜓)) | ||
Theorem | dfor2 932 | Logical 'or' expressed in terms of implication only. Theorem *5.25 of [WhiteheadRussell] p. 124. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Wolf Lammen, 20-Oct-2012.) |
⊢ ((𝜑 ∨ 𝜓) ↔ ((𝜑 → 𝜓) → 𝜓)) | ||
Theorem | pm2.07 933 | Theorem *2.07 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 → (𝜑 ∨ 𝜑)) | ||
Theorem | pm1.2 934 | Axiom *1.2 of [WhiteheadRussell] p. 96, which they call "Taut". (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ 𝜑) → 𝜑) | ||
Theorem | oridm 935 | Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) (Proof shortened by Andrew Salmon, 16-Apr-2011.) (Proof shortened by Wolf Lammen, 10-Mar-2013.) |
⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑) | ||
Theorem | pm4.25 936 | Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 ↔ (𝜑 ∨ 𝜑)) | ||
Theorem | pm2.4 937 | Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓)) | ||
Theorem | pm2.41 938 | Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜓 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓)) | ||
Theorem | orim12i 939 | Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)) | ||
Theorem | orim1i 940 | Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜒)) | ||
Theorem | orim2i 941 | Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) | ||
Theorem | orim12dALT 942 | Alternate proof of orim12d 994 which does not depend on df-an 387. This is an illustration of the conservativity of definitions (definitions do not permit to prove additional theorems whose statements do not contain the defined symbol). (Contributed by Wolf Lammen, 8-Aug-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) | ||
Theorem | orbi2i 943 | Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) | ||
Theorem | orbi1i 944 | Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) | ||
Theorem | orbi12i 945 | Infer the disjunction of two equivalences. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) | ||
Theorem | orbi2d 946 | Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) | ||
Theorem | orbi1d 947 | Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) | ||
Theorem | orbi1 948 | Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))) | ||
Theorem | orbi12d 949 | Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏))) | ||
Theorem | pm1.5 950 | Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜓 ∨ (𝜑 ∨ 𝜒))) | ||
Theorem | or12 951 | Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ (𝜓 ∨ (𝜑 ∨ 𝜒))) | ||
Theorem | orass 952 | Associative law for disjunction. Theorem *4.33 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | ||
Theorem | pm2.31 953 | Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → ((𝜑 ∨ 𝜓) ∨ 𝜒)) | ||
Theorem | pm2.32 954 | Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜑 ∨ (𝜓 ∨ 𝜒))) | ||
Theorem | pm2.3 955 | Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜑 ∨ (𝜒 ∨ 𝜓))) | ||
Theorem | or32 956 | A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜓)) | ||
Theorem | or4 957 | Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜃))) | ||
Theorem | or42 958 | Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.) |
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜃 ∨ 𝜓))) | ||
Theorem | orordi 959 | Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜒))) | ||
Theorem | orordir 960 | Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜒))) | ||
Theorem | orimdi 961 | Disjunction distributes over implication. (Contributed by Wolf Lammen, 5-Jan-2013.) |
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) ↔ ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.76 962 | Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.85 963 | Theorem *2.85 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
⊢ (((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)) → (𝜑 ∨ (𝜓 → 𝜒))) | ||
Theorem | pm2.75 964 | Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.) |
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm4.78 965 | Implication distributes over disjunction. Theorem *4.78 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2012.) |
⊢ (((𝜑 → 𝜓) ∨ (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∨ 𝜒))) | ||
Theorem | biort 966 | A wff disjoined with truth is true. (Contributed by NM, 23-May-1999.) |
⊢ (𝜑 → (𝜑 ↔ (𝜑 ∨ 𝜓))) | ||
Theorem | biorf 967 | A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of [WhiteheadRussell] p. 121. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2012.) |
⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) | ||
Theorem | biortn 968 | A wff is equivalent to its negated disjunction with falsehood. (Contributed by NM, 9-Jul-2012.) |
⊢ (𝜑 → (𝜓 ↔ (¬ 𝜑 ∨ 𝜓))) | ||
Theorem | biorfi 969 | A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 16-Jul-2021.) |
⊢ ¬ 𝜑 ⇒ ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑)) | ||
Theorem | pm2.26 970 | Theorem *2.26 of [WhiteheadRussell] p. 104. See pm2.27 42. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) |
⊢ (¬ 𝜑 ∨ ((𝜑 → 𝜓) → 𝜓)) | ||
Theorem | pm2.63 971 | Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ 𝜓) → ((¬ 𝜑 ∨ 𝜓) → 𝜓)) | ||
Theorem | pm2.64 972 | Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ ¬ 𝜓) → 𝜑)) | ||
Theorem | pm2.42 973 | Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 ∨ (𝜑 → 𝜓)) → (𝜑 → 𝜓)) | ||
Theorem | pm5.11 974 | Theorem *5.11 of [WhiteheadRussell] p. 123. See pm2.5 166. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) ∨ (¬ 𝜑 → 𝜓)) | ||
Theorem | pm5.12 975 | Theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) ∨ (𝜑 → ¬ 𝜓)) | ||
Theorem | pm5.14 976 | Theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) ∨ (𝜓 → 𝜒)) | ||
Theorem | pm5.13 977 | Theorem *5.13 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 14-Nov-2012.) |
⊢ ((𝜑 → 𝜓) ∨ (𝜓 → 𝜑)) | ||
Theorem | pm5.55 978 | Theorem *5.55 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 20-Jan-2013.) |
⊢ (((𝜑 ∨ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∨ 𝜓) ↔ 𝜓)) | ||
Theorem | pm4.72 979 | Implication in terms of biconditional and disjunction. Theorem *4.72 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jan-2013.) |
⊢ ((𝜑 → 𝜓) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓))) | ||
Theorem | imimorb 980 | Simplify an implication between implications. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Wolf Lammen, 3-Apr-2013.) |
⊢ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∨ 𝜒))) | ||
Theorem | oibabs 981 | Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.) |
⊢ (((𝜑 ∨ 𝜓) → (𝜑 ↔ 𝜓)) ↔ (𝜑 ↔ 𝜓)) | ||
Theorem | orbidi 982 | Disjunction distributes over the biconditional. 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 NM, 8-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Feb-2013.) |
⊢ ((𝜑 ∨ (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ 𝜒))) | ||
Theorem | pm5.7 983 | Disjunction distributes over the biconditional. Theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbidi 982. (Contributed by Roy F. Longton, 21-Jun-2005.) |
⊢ (((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) ↔ (𝜒 ∨ (𝜑 ↔ 𝜓))) | ||
This section gathers theorems of propositional calculus which use (either in their statement or proof) mixed connectives (at least conjunction and disjunction). As noted in the "note on definitions" in the section comment for logical equivalence, some theorem statements may contain for instance only conjunction or only disjunction, but both definitions are used in their proofs to make them shorter (this is exemplified in orim12d 994 versus orim12dALT 942). These theorems are mostly grouped at the beginning of this section. The family of theorems starting with animorl 1007 focus on the relation between conjunction and disjunction and can be seen as the starting point of mixed connectives in statements. This sectioning is not rigorously true, since for instance the section begins with jaao 984 and related theorems. | ||
Theorem | jaao 984 | Inference conjoining and disjoining the antecedents of two implications. (Contributed by NM, 30-Sep-1999.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∨ 𝜏) → 𝜒)) | ||
Theorem | jaoa 985 | Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜒)) ⇒ ⊢ ((𝜑 ∨ 𝜃) → ((𝜓 ∧ 𝜏) → 𝜒)) | ||
Theorem | jaoian 986 | Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜃 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒) | ||
Theorem | jaodan 987 | Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜒) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒) | ||
Theorem | mpjaodan 988 | Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 27817. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜒) & ⊢ (𝜑 → (𝜓 ∨ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm3.44 989 | Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) → ((𝜓 ∨ 𝜒) → 𝜑)) | ||
Theorem | jao 990 | Disjunction of antecedents. Compare Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 4-Apr-2013.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜓) → ((𝜑 ∨ 𝜒) → 𝜓))) | ||
Theorem | jaob 991 | Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 9-Dec-2012.) |
⊢ (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓))) | ||
Theorem | pm4.77 992 | Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) ↔ ((𝜓 ∨ 𝜒) → 𝜑)) | ||
Theorem | pm3.48 993 | Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))) | ||
Theorem | orim12d 994 | Disjoin antecedents and consequents in a deduction. See orim12dALT 942 for a proof which does not depend on df-an 387. (Contributed by NM, 10-May-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) | ||
Theorem | orim1d 995 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃))) | ||
Theorem | orim2d 996 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒))) | ||
Theorem | orim2 997 | Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.38 998 | Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
⊢ ((𝜓 → 𝜒) → ((𝜓 ∨ 𝜑) → (𝜒 ∨ 𝜑))) | ||
Theorem | pm2.36 999 | Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
⊢ ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → (𝜒 ∨ 𝜑))) | ||
Theorem | pm2.37 1000 | Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
⊢ ((𝜓 → 𝜒) → ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜒))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |