Home | Metamath
Proof Explorer Theorem List (p. 445 of 466) | < 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-29280) |
Hilbert Space Explorer
(29281-30803) |
Users' Mathboxes
(30804-46521) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | aibnbna 44401 | Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ ¬ 𝜓 ⇒ ⊢ ¬ 𝜑 | ||
Theorem | aibnbaif 44402 | Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ ¬ 𝜓 ⇒ ⊢ (𝜑 ↔ ⊥) | ||
Theorem | aiffbtbat 44403 | 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 44404 | 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 44405 | 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 44406 | Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ¬ (𝜑 ⊻ 𝜓) | ||
Theorem | atbiffatnnb 44407 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓)) | ||
Theorem | bisaiaisb 44408 | Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓)) | ||
Theorem | atbiffatnnbalt 44409 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓)) | ||
Theorem | abnotbtaxb 44410 | Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
⊢ 𝜑 & ⊢ ¬ 𝜓 ⇒ ⊢ (𝜑 ⊻ 𝜓) | ||
Theorem | abnotataxb 44411 | Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
⊢ ¬ 𝜑 & ⊢ 𝜓 ⇒ ⊢ (𝜑 ⊻ 𝜓) | ||
Theorem | conimpf 44412 | 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 44413 | 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 44414 | 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 44415 | 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 44416 | 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 44417 | 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 44418 | Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
⊢ 𝜑 ⇒ ⊢ ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑)) | ||
Theorem | ainaiaandna 44419 | Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
⊢ 𝜑 ⇒ ⊢ (𝜑 → ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑))) | ||
Theorem | abcdta 44420 | Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜑 | ||
Theorem | abcdtb 44421 | Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜓 | ||
Theorem | abcdtc 44422 | Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜒 | ||
Theorem | abcdtd 44423 | Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | abciffcbatnabciffncba 44424 | 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 44425 | Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑)) ⇒ ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑)) | ||
Theorem | nabctnabc 44426 | not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.) |
⊢ ¬ (𝜑 → (𝜓 ∧ 𝜒)) ⇒ ⊢ (¬ 𝜑 → (𝜓 ∧ 𝜒)) | ||
Theorem | jabtaib 44427 | For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.) |
⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | onenotinotbothi 44428 | 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 44429 | 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 44430 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
⊢ (𝜑 ∧ ¬ 𝜒) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒))) | ||
Theorem | cliftet 44431 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
⊢ (𝜑 ∧ 𝜒) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) | ||
Theorem | clifteta 44432 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
⊢ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒)) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒))) | ||
Theorem | cliftetb 44433 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
⊢ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒)) & ⊢ 𝜃 ⇒ ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) | ||
Theorem | confun 44434 | Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020.) |
⊢ 𝜑 & ⊢ (𝜒 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜑 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜒 → (𝜃 ↔ 𝜑)) | ||
Theorem | confun2 44435 | Confun simplified to two propositions. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
⊢ (𝜓 → 𝜑) & ⊢ (𝜓 → ¬ (𝜓 → (𝜓 ∧ ¬ 𝜓))) & ⊢ ((𝜓 → 𝜑) → ((𝜓 → 𝜑) → 𝜑)) ⇒ ⊢ (𝜓 → (¬ (𝜓 → (𝜓 ∧ ¬ 𝜓)) ↔ (𝜓 → 𝜑))) | ||
Theorem | confun3 44436 | Confun's more complex form where both a,d have been "defined". (Contributed by Jarvin Udandy, 6-Sep-2020.) |
⊢ (𝜑 ↔ (𝜒 → 𝜓)) & ⊢ (𝜃 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ (𝜒 → 𝜓) & ⊢ (𝜒 → ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ ((𝜒 → 𝜓) → ((𝜒 → 𝜓) → 𝜓)) ⇒ ⊢ (𝜒 → (¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)) ↔ (𝜒 → 𝜓))) | ||
Theorem | confun4 44437 | An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
⊢ 𝜑 & ⊢ ((𝜑 → 𝜓) → 𝜓) & ⊢ (𝜓 → (𝜑 → 𝜒)) & ⊢ ((𝜒 → 𝜃) → ((𝜑 → 𝜃) ↔ 𝜓)) & ⊢ (𝜏 ↔ (𝜒 → 𝜃)) & ⊢ (𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) ⇒ ⊢ (𝜒 → (𝜓 → 𝜏)) | ||
Theorem | confun5 44438 | 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 44439 | Given, a,b and a "definition" for c, c is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ 𝜒 | ||
Theorem | pldofph 44440 | Given, a,b c, d, "definition" for e, e is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 ⇒ ⊢ 𝜏 | ||
Theorem | plvcofph 44441 | Given, a,b,d, and "definitions" for c, e, f: f is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏)) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜃 ⇒ ⊢ 𝜂 | ||
Theorem | plvcofphax 44442 | Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑)))) & ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃)))) & ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏)) & ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜃 & ⊢ (𝜁 ↔ ¬ (𝜓 ∧ ¬ 𝜏)) ⇒ ⊢ 𝜁 | ||
Theorem | plvofpos 44443 | rh is derivable because ONLY one of ch, th, ta, et is implied by mu. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
⊢ (𝜒 ↔ (¬ 𝜑 ∧ ¬ 𝜓)) & ⊢ (𝜃 ↔ (¬ 𝜑 ∧ 𝜓)) & ⊢ (𝜏 ↔ (𝜑 ∧ ¬ 𝜓)) & ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓)) & ⊢ (𝜁 ↔ (((((¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜃)) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜒 → 𝜂))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜂))) ∧ ¬ ((𝜇 → 𝜏) ∧ (𝜇 → 𝜂)))) & ⊢ (𝜎 ↔ (((𝜇 → 𝜒) ∨ (𝜇 → 𝜃)) ∨ ((𝜇 → 𝜏) ∨ (𝜇 → 𝜂)))) & ⊢ (𝜌 ↔ (𝜁 ∧ 𝜎)) & ⊢ 𝜁 & ⊢ 𝜎 ⇒ ⊢ 𝜌 | ||
Theorem | mdandyv0 44444 | 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 44445 | 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 44446 | 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 44447 | 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 44448 | 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 44449 | 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 44450 | 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 44451 | 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 44452 | 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 44453 | 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 44454 | 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 44455 | 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 44456 | 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 44457 | 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 44458 | 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 44459 | 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 44460 | 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 44461 | 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 44462 | 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 44463 | 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 44464 | 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 44465 | 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 44466 | 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 44467 | 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 44468 | 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 44469 | 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 44470 | 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 44471 | 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 44472 | 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 44473 | 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 44474 | 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 44475 | 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 44476 | 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 44477 | 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 44478 | 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 44479 | 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 44480 | 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 44481 | 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 44482 | 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 44483 | 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 | mdandyvrx8 44484 | 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 | mdandyvrx9 44485 | 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 | mdandyvrx10 44486 | 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 | mdandyvrx11 44487 | 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 | mdandyvrx12 44488 | 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 | mdandyvrx13 44489 | 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 | mdandyvrx14 44490 | 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 | mdandyvrx15 44491 | 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 | H15NH16TH15IH16 44492 | Given 15 hypotheses and a 16th hypothesis, there exists a proof the 15 imply the 16th. (Contributed by Jarvin Udandy, 8-Sep-2016.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ 𝜏 & ⊢ 𝜂 & ⊢ 𝜁 & ⊢ 𝜎 & ⊢ 𝜌 & ⊢ 𝜇 & ⊢ 𝜆 & ⊢ 𝜅 & ⊢ jph & ⊢ jps & ⊢ jch & ⊢ jth ⇒ ⊢ (((((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ jph) ∧ jps) ∧ jch) → jth) | ||
Theorem | dandysum2p2e4 44493 |
CONTRADICTION PROVED AT 1 + 1 = 2 .
Given the right hypotheses we can prove a dandysum of 2+2=4. The qed step is the value '4' in Decimal BEING IMPLIED by the hypotheses. Note: Values that when added would exceed a 4bit value are not supported. Note: Digits begin from left (least) to right (greatest). E.g., 1000 would be '1', 0100 would be '2', 0010 would be '4'. How to perceive the hypotheses' bits in order: ( th <-> F. ), ( ta <-> F. ) Would be input value X's first bit, and input value Y's first bit. ( et <-> F ), ( ze <-> F. ) would be input value X's second bit, and input value Y's second bit. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
⊢ (𝜑 ↔ (𝜃 ∧ 𝜏)) & ⊢ (𝜓 ↔ (𝜂 ∧ 𝜁)) & ⊢ (𝜒 ↔ (𝜎 ∧ 𝜌)) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊤) & ⊢ (𝜁 ↔ ⊤) & ⊢ (𝜎 ↔ ⊥) & ⊢ (𝜌 ↔ ⊥) & ⊢ (𝜇 ↔ ⊥) & ⊢ (𝜆 ↔ ⊥) & ⊢ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏))) & ⊢ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑)) & ⊢ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓)) & ⊢ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒)) ⇒ ⊢ ((((((((((((((((𝜑 ↔ (𝜃 ∧ 𝜏)) ∧ (𝜓 ↔ (𝜂 ∧ 𝜁))) ∧ (𝜒 ↔ (𝜎 ∧ 𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))) ∧ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥))) | ||
Theorem | mdandysum2p2e4 44494 |
CONTRADICTION PROVED AT 1 + 1 = 2 . Luckily Mario Carneiro did a
successful version of his own.
See Mario's Relevant Work: Half adder and full adder in propositional calculus. Given the right hypotheses we can prove a dandysum of 2+2=4. The qed step is the value '4' in Decimal BEING IMPLIED by the hypotheses. Note: Values that when added would exceed a 4bit value are not supported. Note: Digits begin from left (least) to right (greatest). E.g., 1000 would be '1', 0100 would be '2'. 0010 would be '4'. How to perceive the hypotheses' bits in order: ( th <-> F. ), ( ta <-> F. ) Would be input value X's first bit, and input value Y's first bit. ( et <-> F. ), ( ze <-> F. ) would be input value X's second bit, and input value Y's second bit. In mdandysum2p2e4, one might imagine what jth or jta could be then do the math with their truths. Also limited to the restriction jth, jta are having opposite truths equivalent to the stated truth constants. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
⊢ (jth ↔ ⊥) & ⊢ (jta ↔ ⊤) & ⊢ (𝜑 ↔ (𝜃 ∧ 𝜏)) & ⊢ (𝜓 ↔ (𝜂 ∧ 𝜁)) & ⊢ (𝜒 ↔ (𝜎 ∧ 𝜌)) & ⊢ (𝜃 ↔ jth) & ⊢ (𝜏 ↔ jth) & ⊢ (𝜂 ↔ jta) & ⊢ (𝜁 ↔ jta) & ⊢ (𝜎 ↔ jth) & ⊢ (𝜌 ↔ jth) & ⊢ (𝜇 ↔ jth) & ⊢ (𝜆 ↔ jth) & ⊢ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏))) & ⊢ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑)) & ⊢ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓)) & ⊢ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒)) ⇒ ⊢ ((((((((((((((((𝜑 ↔ (𝜃 ∧ 𝜏)) ∧ (𝜓 ↔ (𝜂 ∧ 𝜁))) ∧ (𝜒 ↔ (𝜎 ∧ 𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))) ∧ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥))) | ||
Theorem | adh-jarrsc 44495 | Replacement of a nested antecedent with an outer antecedent. Commuted simplificated form of elimination of a nested antecedent. Also holds intuitionistically. Polish prefix notation: CCCpqrCsCqr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜃 → (𝜓 → 𝜒))) | ||
Minimal implicational calculus, or intuitionistic implicational calculus, or positive implicational calculus, is the implicational fragment of minimal calculus (which is also the implicational fragment of intuitionistic calculus and of positive calculus). It is sometimes called "C-pure intuitionism" since the letter C is used to denote implication in Polish prefix notation. It can be axiomatized by the inference rule of modus ponens ax-mp 5 together with the axioms { ax-1 6, ax-2 7 } (sometimes written KS), or with { imim1 83, ax-1 6, pm2.43 56 } (written B'KW), or with { imim2 58, pm2.04 90, ax-1 6, pm2.43 56 } (written BCKW), or with the single axiom adh-minim 44496, or with the single axiom adh-minimp 44508. This section proves first adh-minim 44496 from { ax-1 6, ax-2 7 }, followed by the converse, due to Ivo Thomas; and then it proves adh-minimp 44508 from { ax-1 6, ax-2 7 }, also followed by the converse, also due to Ivo Thomas. Sources for this section are * Carew Arthur Meredith, A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170; * Ivo Thomas, On Meredith's sole positive axiom, Notre Dame Journal of Formal Logic, volume XV, number 3, July 1974, page 477, in which the derivations of { ax-1 6, ax-2 7 } from adh-minim 44496 are shortened (compared to Meredith's derivations in the aforementioned paper); * Carew Arthur Meredith and Arthur Norman Prior, Notes on the axiomatics of the propositional calculus, Notre Dame Journal of Formal Logic, volume IV, number 3, July 1963, pages 171--187; and * the webpage https://web.ics.purdue.edu/~dulrich/C-pure-intuitionism-page.htm 44496 on Dolph Edward "Ted" Ulrich's website, where these and other single axioms for the minimal implicational calculus are listed. This entire section also holds intuitionistically. Users of the Polish prefix notation also often use a compact notation for proof derivations known as the D-notation where "D" stands for "condensed Detachment". For instance, "D21" means detaching ax-1 6 from ax-2 7, that is, using modus ponens ax-mp 5 with ax-1 6 as minor premise and ax-2 7 as major premise. When the numbered lemmas surpass 10, dots are added between the numbers. D-strings are accepted by the grammar Dundotted := digit | "D" Dundotted Dundotted ; Ddotted := digit + | "D" Ddotted "." Ddotted ; Dstr := Dundotted | Ddotted . (Contributed by BJ, 11-Apr-2021.) (Revised by ADH, 10-Nov-2023.) | ||
Theorem | adh-minim 44496 | A single axiom for minimal implicational calculus, due to Meredith. Other single axioms of the same length are known, but it is thought to be the minimal length. This is the axiom from Carew Arthur Meredith, A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170. A two-line review by Alonzo Church of this article can be found in The Journal of Symbolic Logic, volume 19, issue 2, June 1954, page 144, https://doi.org/10.2307/2268914. Known as "HI-1" on Dolph Edward "Ted" Ulrich's web page. In the next 6 lemmas and 3 theorems, ax-1 6 and ax-2 7 are derived from this single axiom in 16 detachments (instances of ax-mp 5) in total. Polish prefix notation: CCCpqrCsCCqCrtCqt . (Contributed by ADH, 10-Nov-2023.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜃 → ((𝜓 → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))) | ||
Theorem | adh-minim-ax1-ax2-lem1 44497 | First lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 44496 and ax-mp 5. Polish prefix notation: CpCCqCCrCCsCqtCstuCqu . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ((𝜓 → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜂)) → (𝜓 → 𝜂))) | ||
Theorem | adh-minim-ax1-ax2-lem2 44498 | Second lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 44496 and ax-mp 5. Polish prefix notation: CCpCCqCCrCpsCrstCpt . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → ((𝜓 → ((𝜒 → (𝜑 → 𝜃)) → (𝜒 → 𝜃))) → 𝜏)) → (𝜑 → 𝜏)) | ||
Theorem | adh-minim-ax1-ax2-lem3 44499 | Third lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 44496 and ax-mp 5. Polish prefix notation: CCpCqrCqCsCpr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜃 → (𝜑 → 𝜒)))) | ||
Theorem | adh-minim-ax1-ax2-lem4 44500 | Fourth lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 44496 and ax-mp 5. Polish prefix notation: CCCpqrCCqCrsCqs . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜓 → (𝜒 → 𝜃)) → (𝜓 → 𝜃))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |