| Metamath
Proof Explorer Theorem List (p. 470 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | tworepnotupword 46901 | Concatenation of identical singletons is never an increasing sequence. (Contributed by Ender Ting, 22-Nov-2024.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ¬ (〈“𝐴”〉 ++ 〈“𝐴”〉) ∈ UpWord 𝑆 | ||
| Theorem | upwrdfi 46902* | There is a finite number of strictly increasing sequences of a given length over finite alphabet. Trivially holds for invalid lengths where there're zero matching sequences. (Contributed by Ender Ting, 5-Jan-2024.) |
| ⊢ (𝑆 ∈ Fin → {𝑎 ∈ UpWord 𝑆 ∣ (♯‘𝑎) = 𝑇} ∈ Fin) | ||
| Theorem | evenwodadd 46903 | If an integer is multiplied by its sum with an odd number (thus changing its parity), the result is even. (Contributed by Ender Ting, 30-Apr-2025.) |
| ⊢ (𝜑 → 𝑖 ∈ ℤ) & ⊢ (𝜑 → 𝑗 ∈ ℤ) & ⊢ (𝜑 → ¬ 2 ∥ 𝑗) ⇒ ⊢ (𝜑 → 2 ∥ (𝑖 · (𝑖 + 𝑗))) | ||
| Theorem | hirstL-ax3 46904 | The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of [Mendelson] p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015.) (Proof modification is discouraged.) |
| ⊢ ((¬ 𝜑 → ¬ 𝜓) → ((¬ 𝜑 → 𝜓) → 𝜑)) | ||
| Theorem | ax3h 46905 | Recover ax-3 8 from hirstL-ax3 46904. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑)) | ||
| Theorem | aibandbiaiffaiffb 46906 | A closed form showing (a implies b and b implies a) same-as (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.) |
| ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ (𝜑 ↔ 𝜓)) | ||
| Theorem | aibandbiaiaiffb 46907 | A closed form showing (a implies b and b implies a) implies (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.) |
| ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)) | ||
| Theorem | notatnand 46908 | Do not use. Use intnanr instead. Given not a, there exists a proof for not (a and b). (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ ¬ 𝜑 ⇒ ⊢ ¬ (𝜑 ∧ 𝜓) | ||
| Theorem | aistia 46909 | Given a is equivalent to ⊤, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
| ⊢ (𝜑 ↔ ⊤) ⇒ ⊢ 𝜑 | ||
| Theorem | aisfina 46910 | Given a is equivalent to ⊥, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
| ⊢ (𝜑 ↔ ⊥) ⇒ ⊢ ¬ 𝜑 | ||
| Theorem | bothtbothsame 46911 | Given both a, b are equivalent to ⊤, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ (𝜑 ↔ ⊤) & ⊢ (𝜓 ↔ ⊤) ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
| Theorem | bothfbothsame 46912 | Given both a, b are equivalent to ⊥, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊥) ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
| Theorem | aiffbbtat 46913 | Given a is equivalent to b, b is equivalent to ⊤ there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
| ⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ ⊤) ⇒ ⊢ (𝜑 ↔ ⊤) | ||
| Theorem | aisbbisfaisf 46914 | Given a is equivalent to b, b is equivalent to ⊥ there exists a proof for a is equivalent to F. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
| ⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ ⊥) ⇒ ⊢ (𝜑 ↔ ⊥) | ||
| Theorem | axorbtnotaiffb 46915 | Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1512 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ⊻ 𝜓) ⇒ ⊢ ¬ (𝜑 ↔ 𝜓) | ||
| Theorem | aiffnbandciffatnotciffb 46916 | Given a is equivalent to (not b), c is equivalent to a, there exists a proof for ( not ( c iff b ) ). (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ ¬ 𝜓) & ⊢ (𝜒 ↔ 𝜑) ⇒ ⊢ ¬ (𝜒 ↔ 𝜓) | ||
| Theorem | axorbciffatcxorb 46917 | Given a is equivalent to (not b), c is equivalent to a. there exists a proof for ( c xor b ). (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ⊻ 𝜓) & ⊢ (𝜒 ↔ 𝜑) ⇒ ⊢ (𝜒 ⊻ 𝜓) | ||
| Theorem | aibnbna 46918 | Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.) |
| ⊢ (𝜑 → 𝜓) & ⊢ ¬ 𝜓 ⇒ ⊢ ¬ 𝜑 | ||
| Theorem | aibnbaif 46919 | Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.) |
| ⊢ (𝜑 → 𝜓) & ⊢ ¬ 𝜓 ⇒ ⊢ (𝜑 ↔ ⊥) | ||
| Theorem | aiffbtbat 46920 | Given a is equivalent to b, T. is equivalent to b. there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
| ⊢ (𝜑 ↔ 𝜓) & ⊢ (⊤ ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ ⊤) | ||
| Theorem | astbstanbst 46921 | Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for a and b is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
| ⊢ (𝜑 ↔ ⊤) & ⊢ (𝜓 ↔ ⊤) ⇒ ⊢ ((𝜑 ∧ 𝜓) ↔ ⊤) | ||
| Theorem | aistbistaandb 46922 | Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for (a and b). (Contributed by Jarvin Udandy, 9-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊤) & ⊢ (𝜓 ↔ ⊤) ⇒ ⊢ (𝜑 ∧ 𝜓) | ||
| Theorem | aisbnaxb 46923 | Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.) |
| ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ¬ (𝜑 ⊻ 𝜓) | ||
| Theorem | atbiffatnnb 46924 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.) |
| ⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓)) | ||
| Theorem | bisaiaisb 46925 | Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓)) | ||
| Theorem | atbiffatnnbalt 46926 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
| ⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓)) | ||
| Theorem | abnotbtaxb 46927 | Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ 𝜑 & ⊢ ¬ 𝜓 ⇒ ⊢ (𝜑 ⊻ 𝜓) | ||
| Theorem | abnotataxb 46928 | Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ ¬ 𝜑 & ⊢ 𝜓 ⇒ ⊢ (𝜑 ⊻ 𝜓) | ||
| Theorem | conimpf 46929 | Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 28-Aug-2016.) |
| ⊢ 𝜑 & ⊢ ¬ 𝜓 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 ↔ ⊥) | ||
| Theorem | conimpfalt 46930 | Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 29-Aug-2016.) |
| ⊢ 𝜑 & ⊢ ¬ 𝜓 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 ↔ ⊥) | ||
| Theorem | aistbisfiaxb 46931 | Given a is equivalent to T., Given b is equivalent to F. there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ (𝜑 ↔ ⊤) & ⊢ (𝜓 ↔ ⊥) ⇒ ⊢ (𝜑 ⊻ 𝜓) | ||
| Theorem | aisfbistiaxb 46932 | Given a is equivalent to F., Given b is equivalent to T., there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) ⇒ ⊢ (𝜑 ⊻ 𝜓) | ||
| Theorem | aifftbifffaibif 46933 | Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a implies b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ (𝜑 ↔ ⊤) & ⊢ (𝜓 ↔ ⊥) ⇒ ⊢ ((𝜑 → 𝜓) ↔ ⊥) | ||
| Theorem | aifftbifffaibifff 46934 | Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a iff b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ (𝜑 ↔ ⊤) & ⊢ (𝜓 ↔ ⊥) ⇒ ⊢ ((𝜑 ↔ 𝜓) ↔ ⊥) | ||
| Theorem | atnaiana 46935 | Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ 𝜑 ⇒ ⊢ ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑)) | ||
| Theorem | ainaiaandna 46936 | Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ 𝜑 ⇒ ⊢ (𝜑 → ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑))) | ||
| Theorem | abcdta 46937 | Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜑 | ||
| Theorem | abcdtb 46938 | Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜓 | ||
| Theorem | abcdtc 46939 | Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜒 | ||
| Theorem | abcdtd 46940 | Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜃 | ||
| Theorem | abciffcbatnabciffncba 46941 | Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. Closed form. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑)) | ||
| Theorem | abciffcbatnabciffncbai 46942 | Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑)) ⇒ ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑)) | ||
| Theorem | nabctnabc 46943 | not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ ¬ (𝜑 → (𝜓 ∧ 𝜒)) ⇒ ⊢ (¬ 𝜑 → (𝜓 ∧ 𝜒)) | ||
| Theorem | jabtaib 46944 | For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.) |
| ⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | onenotinotbothi 46945 | From one negated implication it is not the case its nonnegated form and a random others are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
| ⊢ ¬ (𝜑 → 𝜓) ⇒ ⊢ ¬ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) | ||
| Theorem | twonotinotbothi 46946 | From these two negated implications it is not the case their nonnegated forms are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
| ⊢ ¬ (𝜑 → 𝜓) & ⊢ ¬ (𝜒 → 𝜃) ⇒ ⊢ ¬ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) | ||
| Theorem | clifte 46947 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
| ⊢ (𝜑 ∧ ¬ 𝜒) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒))) | ||
| Theorem | cliftet 46948 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
| ⊢ (𝜑 ∧ 𝜒) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) | ||
| Theorem | clifteta 46949 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
| ⊢ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒)) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒))) | ||
| Theorem | cliftetb 46950 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
| ⊢ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒)) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) | ||
| Theorem | confun 46951 | Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020.) |
| ⊢ 𝜑 & ⊢ (𝜒 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜑 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜒 → (𝜃 ↔ 𝜑)) | ||
| Theorem | confun2 46952 | Confun simplified to two propositions. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
| ⊢ (𝜓 → 𝜑) & ⊢ (𝜓 → ¬ (𝜓 → (𝜓 ∧ ¬ 𝜓))) & ⊢ ((𝜓 → 𝜑) → ((𝜓 → 𝜑) → 𝜑)) ⇒ ⊢ (𝜓 → (¬ (𝜓 → (𝜓 ∧ ¬ 𝜓)) ↔ (𝜓 → 𝜑))) | ||
| Theorem | confun3 46953 | Confun's more complex form where both a,d have been "defined". (Contributed by Jarvin Udandy, 6-Sep-2020.) |
| ⊢ (𝜑 ↔ (𝜒 → 𝜓)) & ⊢ (𝜃 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ (𝜒 → 𝜓) & ⊢ (𝜒 → ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ ((𝜒 → 𝜓) → ((𝜒 → 𝜓) → 𝜓)) ⇒ ⊢ (𝜒 → (¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)) ↔ (𝜒 → 𝜓))) | ||
| Theorem | confun4 46954 | An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
| ⊢ 𝜑 & ⊢ ((𝜑 → 𝜓) → 𝜓) & ⊢ (𝜓 → (𝜑 → 𝜒)) & ⊢ ((𝜒 → 𝜃) → ((𝜑 → 𝜃) ↔ 𝜓)) & ⊢ (𝜏 ↔ (𝜒 → 𝜃)) & ⊢ (𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) ⇒ ⊢ (𝜒 → (𝜓 → 𝜏)) | ||
| Theorem | confun5 46955 | An attempt at derivative. Resisted simplest path to a proof. Interesting that ch, th, ta, et were all provable. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
| ⊢ 𝜑 & ⊢ ((𝜑 → 𝜓) → 𝜓) & ⊢ (𝜓 → (𝜑 → 𝜒)) & ⊢ ((𝜒 → 𝜃) → ((𝜑 → 𝜃) ↔ 𝜓)) & ⊢ (𝜏 ↔ (𝜒 → 𝜃)) & ⊢ (𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) ⇒ ⊢ (𝜒 → (𝜂 ↔ 𝜏)) | ||
| Theorem | plcofph 46956 | Given, a,b and a "definition" for c, c is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
| ⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ 𝜒 | ||
| Theorem | pldofph 46957 | Given, a,b c, d, "definition" for e, e is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
| ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 ⇒ ⊢ 𝜏 | ||
| Theorem | plvcofph 46958 | Given, a,b,d, and "definitions" for c, e, f: f is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
| ⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏)) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜃 ⇒ ⊢ 𝜂 | ||
| Theorem | plvcofphax 46959 | Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
| ⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏)) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜃 & ⊢ (𝜁 ↔ ¬ (𝜓 ∧ ¬ 𝜏)) ⇒ ⊢ 𝜁 | ||
| Theorem | plvofpos 46960 | rh is derivable because ONLY one of ch, th, ta, et is implied by mu. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
| ⊢ (𝜒 ↔ (¬ 𝜑 ∧ ¬ 𝜓)) & ⊢ (𝜃 ↔ (¬ 𝜑 ∧ 𝜓)) & ⊢ (𝜏 ↔ (𝜑 ∧ ¬ 𝜓)) & ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓)) & ⊢ (𝜁 ↔ (((((¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜃)) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜒 → 𝜂))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜂))) ∧ ¬ ((𝜇 → 𝜏) ∧ (𝜇 → 𝜂)))) & ⊢ (𝜎 ↔ (((𝜇 → 𝜒) ∨ (𝜇 → 𝜃)) ∨ ((𝜇 → 𝜏) ∨ (𝜇 → 𝜂)))) & ⊢ (𝜌 ↔ (𝜁 ∧ 𝜎)) & ⊢ 𝜁 & ⊢ 𝜎 ⇒ ⊢ 𝜌 | ||
| Theorem | mdandyv0 46961 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊥) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv1 46962 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊤) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv2 46963 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊥) & ⊢ (𝜃 ↔ ⊤) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv3 46964 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊤) & ⊢ (𝜃 ↔ ⊤) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv4 46965 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊥) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊤) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv5 46966 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊤) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊤) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv6 46967 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊥) & ⊢ (𝜃 ↔ ⊤) & ⊢ (𝜏 ↔ ⊤) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv7 46968 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊤) & ⊢ (𝜃 ↔ ⊤) & ⊢ (𝜏 ↔ ⊤) & ⊢ (𝜂 ↔ ⊥) ⇒ ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜑)) | ||
| Theorem | mdandyv8 46969 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊥) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊤) ⇒ ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜓)) | ||
| Theorem | mdandyv9 46970 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊤) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊤) ⇒ ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜓)) | ||
| Theorem | mdandyv10 46971 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊥) & ⊢ (𝜃 ↔ ⊤) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊤) ⇒ ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜓)) | ||
| Theorem | mdandyv11 46972 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊤) & ⊢ (𝜃 ↔ ⊤) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊤) ⇒ ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜓)) | ||
| Theorem | mdandyv12 46973 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊥) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊤) & ⊢ (𝜂 ↔ ⊤) ⇒ ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜓)) | ||
| Theorem | mdandyv13 46974 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊤) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊤) & ⊢ (𝜂 ↔ ⊤) ⇒ ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜓)) | ||
| Theorem | mdandyv14 46975 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊥) & ⊢ (𝜃 ↔ ⊤) & ⊢ (𝜏 ↔ ⊤) & ⊢ (𝜂 ↔ ⊤) ⇒ ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜓)) | ||
| Theorem | mdandyv15 46976 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
| ⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊤) & ⊢ (𝜒 ↔ ⊤) & ⊢ (𝜃 ↔ ⊤) & ⊢ (𝜏 ↔ ⊤) & ⊢ (𝜂 ↔ ⊤) ⇒ ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜓)) | ||
| Theorem | mdandyvr0 46977 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜑) & ⊢ (𝜏 ↔ 𝜑) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜁)) | ||
| Theorem | mdandyvr1 46978 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜑) & ⊢ (𝜏 ↔ 𝜑) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜁)) | ||
| Theorem | mdandyvr2 46979 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜑) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜁)) | ||
| Theorem | mdandyvr3 46980 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜑) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜁)) | ||
| Theorem | mdandyvr4 46981 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜑) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜁)) | ||
| Theorem | mdandyvr5 46982 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜑) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜁)) | ||
| Theorem | mdandyvr6 46983 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜁)) | ||
| Theorem | mdandyvr7 46984 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜁)) | ||
| Theorem | mdandyvr8 46985 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜑) & ⊢ (𝜏 ↔ 𝜑) & ⊢ (𝜂 ↔ 𝜓) ⇒ ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜎)) | ||
| Theorem | mdandyvr9 46986 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜑) & ⊢ (𝜏 ↔ 𝜑) & ⊢ (𝜂 ↔ 𝜓) ⇒ ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜎)) | ||
| Theorem | mdandyvr10 46987 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜑) & ⊢ (𝜂 ↔ 𝜓) ⇒ ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜎)) | ||
| Theorem | mdandyvr11 46988 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜑) & ⊢ (𝜂 ↔ 𝜓) ⇒ ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜎)) | ||
| Theorem | mdandyvr12 46989 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜑) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜓) ⇒ ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜎)) | ||
| Theorem | mdandyvr13 46990 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜑) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜓) ⇒ ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜎)) | ||
| Theorem | mdandyvr14 46991 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜓) ⇒ ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜎)) | ||
| Theorem | mdandyvr15 46992 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ↔ 𝜁) & ⊢ (𝜓 ↔ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜓) ⇒ ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜎)) | ||
| Theorem | mdandyvrx0 46993 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ⊻ 𝜁) & ⊢ (𝜓 ⊻ 𝜎) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜑) & ⊢ (𝜏 ↔ 𝜑) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ⊻ 𝜁) ∧ (𝜃 ⊻ 𝜁)) ∧ (𝜏 ⊻ 𝜁)) ∧ (𝜂 ⊻ 𝜁)) | ||
| Theorem | mdandyvrx1 46994 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ⊻ 𝜁) & ⊢ (𝜓 ⊻ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜑) & ⊢ (𝜏 ↔ 𝜑) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜁)) ∧ (𝜏 ⊻ 𝜁)) ∧ (𝜂 ⊻ 𝜁)) | ||
| Theorem | mdandyvrx2 46995 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ⊻ 𝜁) & ⊢ (𝜓 ⊻ 𝜎) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜑) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ⊻ 𝜁) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜁)) ∧ (𝜂 ⊻ 𝜁)) | ||
| Theorem | mdandyvrx3 46996 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ⊻ 𝜁) & ⊢ (𝜓 ⊻ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜑) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜁)) ∧ (𝜂 ⊻ 𝜁)) | ||
| Theorem | mdandyvrx4 46997 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ⊻ 𝜁) & ⊢ (𝜓 ⊻ 𝜎) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜑) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ⊻ 𝜁) ∧ (𝜃 ⊻ 𝜁)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜁)) | ||
| Theorem | mdandyvrx5 46998 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ⊻ 𝜁) & ⊢ (𝜓 ⊻ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜑) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜁)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜁)) | ||
| Theorem | mdandyvrx6 46999 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ⊻ 𝜁) & ⊢ (𝜓 ⊻ 𝜎) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ⊻ 𝜁) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜁)) | ||
| Theorem | mdandyvrx7 47000 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
| ⊢ (𝜑 ⊻ 𝜁) & ⊢ (𝜓 ⊻ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜑) ⇒ ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜁)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |