![]() |
Metamath
Proof Explorer Theorem List (p. 457 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | upwrdfi 45601* | 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 | hirstL-ax3 45602 | 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 45603 | Recover ax-3 8 from hirstL-ax3 45602. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((Β¬ π β Β¬ π) β (π β π)) | ||
Theorem | aibandbiaiffaiffb 45604 | 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 45605 | 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 45606 | 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 45607 | Given a is equivalent to β€, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
β’ (π β β€) β β’ π | ||
Theorem | aisfina 45608 | Given a is equivalent to β₯, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
β’ (π β β₯) β β’ Β¬ π | ||
Theorem | bothtbothsame 45609 | 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 45610 | 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 45611 | 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 45612 | 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 45613 | Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1511 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
β’ (π β» π) β β’ Β¬ (π β π) | ||
Theorem | aiffnbandciffatnotciffb 45614 | 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 45615 | 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 45616 | Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.) |
β’ (π β π) & β’ Β¬ π β β’ Β¬ π | ||
Theorem | aibnbaif 45617 | Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.) |
β’ (π β π) & β’ Β¬ π β β’ (π β β₯) | ||
Theorem | aiffbtbat 45618 | 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 45619 | 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 45620 | 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 45621 | Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.) |
β’ (π β π) β β’ Β¬ (π β» π) | ||
Theorem | atbiffatnnb 45622 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.) |
β’ ((π β π) β (π β Β¬ Β¬ π)) | ||
Theorem | bisaiaisb 45623 | Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ ((π β π) β (π β π)) | ||
Theorem | atbiffatnnbalt 45624 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
β’ ((π β π) β (π β Β¬ Β¬ π)) | ||
Theorem | abnotbtaxb 45625 | Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ π & β’ Β¬ π β β’ (π β» π) | ||
Theorem | abnotataxb 45626 | Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ Β¬ π & β’ π β β’ (π β» π) | ||
Theorem | conimpf 45627 | 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 45628 | 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 45629 | 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 45630 | 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 45631 | 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 45632 | 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 45633 | Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
β’ π β β’ Β¬ (π β (π β§ Β¬ π)) | ||
Theorem | ainaiaandna 45634 | Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
β’ π β β’ (π β Β¬ (π β (π β§ Β¬ π))) | ||
Theorem | abcdta 45635 | Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
β’ (((π β§ π) β§ π) β§ π) β β’ π | ||
Theorem | abcdtb 45636 | Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
β’ (((π β§ π) β§ π) β§ π) β β’ π | ||
Theorem | abcdtc 45637 | Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
β’ (((π β§ π) β§ π) β§ π) β β’ π | ||
Theorem | abcdtd 45638 | Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
β’ (((π β§ π) β§ π) β§ π) β β’ π | ||
Theorem | abciffcbatnabciffncba 45639 | 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 45640 | Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
β’ (((π β§ π) β§ π) β ((π β§ π) β§ π)) β β’ (Β¬ ((π β§ π) β§ π) β Β¬ ((π β§ π) β§ π)) | ||
Theorem | nabctnabc 45641 | not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.) |
β’ Β¬ (π β (π β§ π)) β β’ (Β¬ π β (π β§ π)) | ||
Theorem | jabtaib 45642 | For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.) |
β’ (π β§ π) β β’ (π β π) | ||
Theorem | onenotinotbothi 45643 | 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 45644 | 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 45645 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
β’ (π β§ Β¬ π) & β’ π β β’ (π β ((π β§ Β¬ π) β¨ (π β§ π))) | ||
Theorem | cliftet 45646 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
β’ (π β§ π) & β’ π β β’ (π β ((π β§ π) β¨ (π β§ Β¬ π))) | ||
Theorem | clifteta 45647 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
β’ ((π β§ Β¬ π) β¨ (π β§ π)) & β’ π β β’ (π β ((π β§ Β¬ π) β¨ (π β§ π))) | ||
Theorem | cliftetb 45648 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
β’ ((π β§ π) β¨ (π β§ Β¬ π)) & β’ π β β’ (π β ((π β§ π) β¨ (π β§ Β¬ π))) | ||
Theorem | confun 45649 | Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020.) |
β’ π & β’ (π β π) & β’ (π β π) & β’ (π β (π β π)) β β’ (π β (π β π)) | ||
Theorem | confun2 45650 | Confun simplified to two propositions. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
β’ (π β π) & β’ (π β Β¬ (π β (π β§ Β¬ π))) & β’ ((π β π) β ((π β π) β π)) β β’ (π β (Β¬ (π β (π β§ Β¬ π)) β (π β π))) | ||
Theorem | confun3 45651 | Confun's more complex form where both a,d have been "defined". (Contributed by Jarvin Udandy, 6-Sep-2020.) |
β’ (π β (π β π)) & β’ (π β Β¬ (π β (π β§ Β¬ π))) & β’ (π β π) & β’ (π β Β¬ (π β (π β§ Β¬ π))) & β’ ((π β π) β ((π β π) β π)) β β’ (π β (Β¬ (π β (π β§ Β¬ π)) β (π β π))) | ||
Theorem | confun4 45652 | An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
β’ π & β’ ((π β π) β π) & β’ (π β (π β π)) & β’ ((π β π) β ((π β π) β π)) & β’ (π β (π β π)) & β’ (π β Β¬ (π β (π β§ Β¬ π))) & β’ π & β’ (π β π) β β’ (π β (π β π)) | ||
Theorem | confun5 45653 | 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 45654 | Given, a,b and a "definition" for c, c is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
β’ (π β ((((π β§ π) β π) β (π β§ Β¬ (π β§ Β¬ π))) β§ (π β§ Β¬ (π β§ Β¬ π)))) & β’ π & β’ π β β’ π | ||
Theorem | pldofph 45655 | Given, a,b c, d, "definition" for e, e is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
β’ (π β ((π β π) β§ (π β π) β§ ((π β π) β (π β π)))) & β’ π & β’ π & β’ π & β’ π β β’ π | ||
Theorem | plvcofph 45656 | Given, a,b,d, and "definitions" for c, e, f: f is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
β’ (π β ((((π β§ π) β π) β (π β§ Β¬ (π β§ Β¬ π))) β§ (π β§ Β¬ (π β§ Β¬ π)))) & β’ (π β ((π β π) β§ (π β π) β§ ((π β π) β (π β π)))) & β’ (π β (π β§ π)) & β’ π & β’ π & β’ π β β’ π | ||
Theorem | plvcofphax 45657 | Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
β’ (π β ((((π β§ π) β π) β (π β§ Β¬ (π β§ Β¬ π))) β§ (π β§ Β¬ (π β§ Β¬ π)))) & β’ (π β ((π β π) β§ (π β π) β§ ((π β π) β (π β π)))) & β’ (π β (π β§ π)) & β’ π & β’ π & β’ π & β’ (π β Β¬ (π β§ Β¬ π)) β β’ π | ||
Theorem | plvofpos 45658 | rh is derivable because ONLY one of ch, th, ta, et is implied by mu. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
β’ (π β (Β¬ π β§ Β¬ π)) & β’ (π β (Β¬ π β§ π)) & β’ (π β (π β§ Β¬ π)) & β’ (π β (π β§ π)) & β’ (π β (((((Β¬ ((π β π) β§ (π β π)) β§ Β¬ ((π β π) β§ (π β π))) β§ Β¬ ((π β π) β§ (π β π))) β§ Β¬ ((π β π) β§ (π β π))) β§ Β¬ ((π β π) β§ (π β π))) β§ Β¬ ((π β π) β§ (π β π)))) & β’ (π β (((π β π) β¨ (π β π)) β¨ ((π β π) β¨ (π β π)))) & β’ (π β (π β§ π)) & β’ π & β’ π β β’ π | ||
Theorem | mdandyv0 45659 | 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 45660 | 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 45661 | 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 45662 | 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 45663 | 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 45664 | 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 45665 | 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 45666 | 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 45667 | 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 45668 | 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 45669 | 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 45670 | 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 45671 | 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 45672 | 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 45673 | 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 45674 | 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 45675 | 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 45676 | 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 45677 | 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 45678 | 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 45679 | 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 45680 | 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 45681 | 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 45682 | 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 45683 | 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 45684 | 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 45685 | 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 45686 | 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 45687 | 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 45688 | 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 45689 | 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 45690 | 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 45691 | 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 45692 | 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 45693 | 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 45694 | 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 45695 | 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 45696 | 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 45697 | 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 45698 | 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 45699 | 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 45700 | 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 > |