Home | Metamath
Proof Explorer Theorem List (p. 398 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sigariz 39701* | If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) & ⊢ (𝜑 → (𝐴𝐺𝐵) = 0) ⇒ ⊢ (𝜑 → (𝐵𝐺𝐴) = 0) | ||
Theorem | sigarcol 39702* | Given three points 𝐴, 𝐵 and 𝐶 such that ¬ 𝐴 = 𝐵, the point 𝐶 lies on the line going through 𝐴 and 𝐵 iff the corresponding signed area is zero. That justifies the usage of signed area as a collinearity indicator. (Contributed by Saveliy Skresanov, 22-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (((𝐴 − 𝐶)𝐺(𝐵 − 𝐶)) = 0 ↔ ∃𝑡 ∈ ℝ 𝐶 = (𝐵 + (𝑡 · (𝐴 − 𝐵))))) | ||
Theorem | sharhght 39703* | Let 𝐴𝐵𝐶 be a triangle, and let 𝐷 lie on the line 𝐴𝐵. Then (doubled) areas of triangles 𝐴𝐷𝐶 and 𝐶𝐷𝐵 relate as lengths of corresponding bases 𝐴𝐷 and 𝐷𝐵. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0)) ⇒ ⊢ (𝜑 → (((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) · (𝐵 − 𝐷)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · (𝐴 − 𝐷))) | ||
Theorem | sigaradd 39704* | Subtracting (double) area of 𝐴𝐷𝐶 from 𝐴𝐵𝐶 yields the (double) area of 𝐷𝐵𝐶. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0)) ⇒ ⊢ (𝜑 → (((𝐵 − 𝐶)𝐺(𝐴 − 𝐶)) − ((𝐷 − 𝐶)𝐺(𝐴 − 𝐶))) = ((𝐵 − 𝐶)𝐺(𝐷 − 𝐶))) | ||
Theorem | cevathlem1 39705 | Ceva's theorem first lemma. Multiplies three identities and divides by the common factors. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) & ⊢ (𝜑 → (𝐺 ∈ ℂ ∧ 𝐻 ∈ ℂ ∧ 𝐾 ∈ ℂ)) & ⊢ (𝜑 → (𝐴 ≠ 0 ∧ 𝐸 ≠ 0 ∧ 𝐶 ≠ 0)) & ⊢ (𝜑 → ((𝐴 · 𝐵) = (𝐶 · 𝐷) ∧ (𝐸 · 𝐹) = (𝐴 · 𝐺) ∧ (𝐶 · 𝐻) = (𝐸 · 𝐾))) ⇒ ⊢ (𝜑 → ((𝐵 · 𝐹) · 𝐻) = ((𝐷 · 𝐺) · 𝐾)) | ||
Theorem | cevathlem2 39706* | Ceva's theorem second lemma. Relate (doubled) areas of triangles 𝐶𝐴𝑂 and 𝐴𝐵𝑂 with of segments 𝐵𝐷 and 𝐷𝐶. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ)) & ⊢ (𝜑 → 𝑂 ∈ ℂ) & ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐷 − 𝑂)) = 0 ∧ ((𝐵 − 𝑂)𝐺(𝐸 − 𝑂)) = 0 ∧ ((𝐶 − 𝑂)𝐺(𝐹 − 𝑂)) = 0)) & ⊢ (𝜑 → (((𝐴 − 𝐹)𝐺(𝐵 − 𝐹)) = 0 ∧ ((𝐵 − 𝐷)𝐺(𝐶 − 𝐷)) = 0 ∧ ((𝐶 − 𝐸)𝐺(𝐴 − 𝐸)) = 0)) & ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) ≠ 0 ∧ ((𝐵 − 𝑂)𝐺(𝐶 − 𝑂)) ≠ 0 ∧ ((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) ≠ 0)) ⇒ ⊢ (𝜑 → (((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) · (𝐵 − 𝐷)) = (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) · (𝐷 − 𝐶))) | ||
Theorem | cevath 39707* |
Ceva's theorem. Let 𝐴𝐵𝐶 be a triangle and let points 𝐹,
𝐷 and 𝐸 lie on sides 𝐴𝐵, 𝐵𝐶, 𝐶𝐴
correspondingly. Suppose that cevians 𝐴𝐷, 𝐵𝐸 and 𝐶𝐹
intersect at one point 𝑂. Then triangle's sides are
partitioned
into segments and their lengths satisfy a certain identity. Here we
obtain a bit stronger version by using complex numbers themselves
instead of their absolute values.
The proof goes by applying cevathlem2 39706 three times and then using cevathlem1 39705 to multiply obtained identities and prove the theorem. In the theorem statement we are using function 𝐺 as a collinearity indicator. For justification of that use, see sigarcol 39702. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ)) & ⊢ (𝜑 → 𝑂 ∈ ℂ) & ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐷 − 𝑂)) = 0 ∧ ((𝐵 − 𝑂)𝐺(𝐸 − 𝑂)) = 0 ∧ ((𝐶 − 𝑂)𝐺(𝐹 − 𝑂)) = 0)) & ⊢ (𝜑 → (((𝐴 − 𝐹)𝐺(𝐵 − 𝐹)) = 0 ∧ ((𝐵 − 𝐷)𝐺(𝐶 − 𝐷)) = 0 ∧ ((𝐶 − 𝐸)𝐺(𝐴 − 𝐸)) = 0)) & ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) ≠ 0 ∧ ((𝐵 − 𝑂)𝐺(𝐶 − 𝑂)) ≠ 0 ∧ ((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) ≠ 0)) ⇒ ⊢ (𝜑 → (((𝐴 − 𝐹) · (𝐶 − 𝐸)) · (𝐵 − 𝐷)) = (((𝐹 − 𝐵) · (𝐸 − 𝐴)) · (𝐷 − 𝐶))) | ||
Theorem | hirstL-ax3 39708 | 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 39709 | Recovery of ax-3 8 from hirstL-ax3 39708. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑)) | ||
Theorem | aibandbiaiffaiffb 39710 | 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 39711 | 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 39712 | 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 39713 | Given a is equivalent to ⊤, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
⊢ (𝜑 ↔ ⊤) ⇒ ⊢ 𝜑 | ||
Theorem | aisfina 39714 | Given a is equivalent to ⊥, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
⊢ (𝜑 ↔ ⊥) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | bothtbothsame 39715 | 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 39716 | 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 39717 | 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 39718 | 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 39719 | Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1457 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
⊢ (𝜑 ⊻ 𝜓) ⇒ ⊢ ¬ (𝜑 ↔ 𝜓) | ||
Theorem | aiffnbandciffatnotciffb 39720 | 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 39721 | 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 39722 | Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ ¬ 𝜓 ⇒ ⊢ ¬ 𝜑 | ||
Theorem | aibnbaif 39723 | Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ ¬ 𝜓 ⇒ ⊢ (𝜑 ↔ ⊥) | ||
Theorem | aiffbtbat 39724 | 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 39725 | 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 39726 | 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 39727 | Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ¬ (𝜑 ⊻ 𝜓) | ||
Theorem | atbiffatnnb 39728 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓)) | ||
Theorem | bisaiaisb 39729 | Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓)) | ||
Theorem | atbiffatnnbalt 39730 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓)) | ||
Theorem | abnotbtaxb 39731 | Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
⊢ 𝜑 & ⊢ ¬ 𝜓 ⇒ ⊢ (𝜑 ⊻ 𝜓) | ||
Theorem | abnotataxb 39732 | Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
⊢ ¬ 𝜑 & ⊢ 𝜓 ⇒ ⊢ (𝜑 ⊻ 𝜓) | ||
Theorem | conimpf 39733 | 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 39734 | 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 39735 | 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 39736 | 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 39737 | 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 39738 | 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 39739 | Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
⊢ 𝜑 ⇒ ⊢ ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑)) | ||
Theorem | ainaiaandna 39740 | Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
⊢ 𝜑 ⇒ ⊢ (𝜑 → ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑))) | ||
Theorem | abcdta 39741 | Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜑 | ||
Theorem | abcdtb 39742 | Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜓 | ||
Theorem | abcdtc 39743 | Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜒 | ||
Theorem | abcdtd 39744 | Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | abciffcbatnabciffncba 39745 | 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 39746 | Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑)) ⇒ ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑)) | ||
Theorem | nabctnabc 39747 | not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.) |
⊢ ¬ (𝜑 → (𝜓 ∧ 𝜒)) ⇒ ⊢ (¬ 𝜑 → (𝜓 ∧ 𝜒)) | ||
Theorem | jabtaib 39748 | For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.) |
⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | onenotinotbothi 39749 | From one negated implication it is not the case its non negated form and a random others are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
⊢ ¬ (𝜑 → 𝜓) ⇒ ⊢ ¬ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) | ||
Theorem | twonotinotbothi 39750 | From these two negated implications it is not the case their non negated forms are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
⊢ ¬ (𝜑 → 𝜓) & ⊢ ¬ (𝜒 → 𝜃) ⇒ ⊢ ¬ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) | ||
Theorem | clifte 39751 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
⊢ (𝜑 ∧ ¬ 𝜒) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒))) | ||
Theorem | cliftet 39752 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
⊢ (𝜑 ∧ 𝜒) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) | ||
Theorem | clifteta 39753 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
⊢ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒)) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒))) | ||
Theorem | cliftetb 39754 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
⊢ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒)) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) | ||
Theorem | confun 39755 | Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020.) |
⊢ 𝜑 & ⊢ (𝜒 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜑 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜒 → (𝜃 ↔ 𝜑)) | ||
Theorem | confun2 39756 | Confun simplified to two propositions. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
⊢ (𝜓 → 𝜑) & ⊢ (𝜓 → ¬ (𝜓 → (𝜓 ∧ ¬ 𝜓))) & ⊢ ((𝜓 → 𝜑) → ((𝜓 → 𝜑) → 𝜑)) ⇒ ⊢ (𝜓 → (¬ (𝜓 → (𝜓 ∧ ¬ 𝜓)) ↔ (𝜓 → 𝜑))) | ||
Theorem | confun3 39757 | Confun's more complex form where both a,d have been "defined". (Contributed by Jarvin Udandy, 6-Sep-2020.) |
⊢ (𝜑 ↔ (𝜒 → 𝜓)) & ⊢ (𝜃 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ (𝜒 → 𝜓) & ⊢ (𝜒 → ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ ((𝜒 → 𝜓) → ((𝜒 → 𝜓) → 𝜓)) ⇒ ⊢ (𝜒 → (¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)) ↔ (𝜒 → 𝜓))) | ||
Theorem | confun4 39758 | An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
⊢ 𝜑 & ⊢ ((𝜑 → 𝜓) → 𝜓) & ⊢ (𝜓 → (𝜑 → 𝜒)) & ⊢ ((𝜒 → 𝜃) → ((𝜑 → 𝜃) ↔ 𝜓)) & ⊢ (𝜏 ↔ (𝜒 → 𝜃)) & ⊢ (𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) ⇒ ⊢ (𝜒 → (𝜓 → 𝜏)) | ||
Theorem | confun5 39759 | 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 39760 | Given, a,b and a "definition" for c, c is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ 𝜒 | ||
Theorem | pldofph 39761 | Given, a,b c, d, "definition" for e, e is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 ⇒ ⊢ 𝜏 | ||
Theorem | plvcofph 39762 | Given, a,b,d, and "definitions" for c, e, f: f is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏)) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜃 ⇒ ⊢ 𝜂 | ||
Theorem | plvcofphax 39763 | Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏)) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜃 & ⊢ (𝜁 ↔ ¬ (𝜓 ∧ ¬ 𝜏)) ⇒ ⊢ 𝜁 | ||
Theorem | plvofpos 39764 | rh is derivable because ONLY one of ch, th, ta, et is implied by mu. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
⊢ (𝜒 ↔ (¬ 𝜑 ∧ ¬ 𝜓)) & ⊢ (𝜃 ↔ (¬ 𝜑 ∧ 𝜓)) & ⊢ (𝜏 ↔ (𝜑 ∧ ¬ 𝜓)) & ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓)) & ⊢ (𝜁 ↔ (((((¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜃)) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜒 → 𝜂))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜂))) ∧ ¬ ((𝜇 → 𝜏) ∧ (𝜇 → 𝜂)))) & ⊢ (𝜎 ↔ (((𝜇 → 𝜒) ∨ (𝜇 → 𝜃)) ∨ ((𝜇 → 𝜏) ∨ (𝜇 → 𝜂)))) & ⊢ (𝜌 ↔ (𝜁 ∧ 𝜎)) & ⊢ 𝜁 & ⊢ 𝜎 ⇒ ⊢ 𝜌 | ||
Theorem | mdandyv0 39765 | 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 39766 | 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 39767 | 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 39768 | 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 39769 | 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 39770 | 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 39771 | 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 39772 | 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 39773 | 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 39774 | 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 39775 | 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 39776 | 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 39777 | 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 39778 | 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 39779 | 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 39780 | 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 39781 | 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 39782 | 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 39783 | 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 39784 | 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 39785 | 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 39786 | 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 39787 | 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 39788 | 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 39789 | 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 39790 | 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 39791 | 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 39792 | 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 39793 | 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 39794 | 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 39795 | 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 39796 | 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 39797 | 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 39798 | 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 39799 | 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 39800 | 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 > |