Home | Metamath
Proof Explorer Theorem List (p. 7 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pm4.44 601 | Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm4.14 602 | Theorem *4.14 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Oct-2012.) |
Theorem | pm3.37 603 | Theorem *3.37 (Transp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Oct-2012.) |
Theorem | nan 604 | Theorem to move a conjunct in and out of a negation. (Contributed by NM, 9-Nov-2003.) |
Theorem | pm4.15 605 | Theorem *4.15 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 18-Nov-2012.) |
Theorem | pm4.78 606 | Implication distributes over disjunction. Theorem *4.78 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2012.) |
Theorem | pm4.79 607 | Theorem *4.79 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 27-Jun-2013.) |
Theorem | pm4.87 608 | Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Eric Schmidt, 26-Oct-2006.) |
Theorem | pm3.33 609 | Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm3.34 610 | Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm3.35 611 | Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. (Contributed by NM, 14-Dec-2002.) |
Theorem | pm5.31 612 | Theorem *5.31 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
Theorem | imp4b 613 | An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 614. (Revised by Wolf Lammen, 19-Jul-2021.) |
Theorem | imp4a 614 | An importation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Jul-2021.) |
Theorem | imp4aOLD 615 | Obsolete proof of imp4a 614 as of 19-Jul-2021. (Contributed by NM, 26-Apr-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | imp4bOLD 616 | Obsolete proof of imp4b 613 as of 19-Jul-2021. (Contributed by NM, 26-Apr-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | imp4c 617 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | imp4d 618 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | imp41 619 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | imp42 620 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | imp43 621 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | imp44 622 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | imp45 623 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | imp5a 624 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
Theorem | imp5d 625 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
Theorem | imp5g 626 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
Theorem | imp55 627 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
Theorem | imp511 628 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
Theorem | expimpd 629 | Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.) |
Theorem | exp31 630 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | exp32 631 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | exp4b 632 | An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 633. (Revised by Wolf Lammen, 20-Jul-2021.) |
Theorem | exp4a 633 | An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2021.) |
Theorem | exp4aOLD 634 | Obsolete proof of exp4a 633 as of 20-Jul-2021. (Contributed by NM, 26-Apr-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | exp4bOLD 635 | Obsolete proof of exp4b 632 as of 20-Jul-2021. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | exp4c 636 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | exp4d 637 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | exp41 638 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | exp42 639 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | exp43 640 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | exp44 641 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | exp45 642 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | expr 643 | Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.) |
Theorem | exp5c 644 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
Theorem | exp5j 645 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
Theorem | exp5l 646 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
Theorem | exp53 647 | An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.) |
Theorem | expl 648 | Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.) |
Theorem | impr 649 | Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.) |
Theorem | impl 650 | Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.) |
Theorem | impac 651 | Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994.) |
Theorem | exbiri 652 | Inference form of exbir 38684. This proof is exbiriVD 39089 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.) |
Theorem | simprbda 653 | Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.) |
Theorem | simplbda 654 | Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.) |
Theorem | simplbi2 655 | Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.) |
Theorem | simplbi2comt 656 | Closed form of simplbi2com 657. (Contributed by Alan Sare, 22-Jul-2012.) |
Theorem | simplbi2com 657 | A deduction eliminating a conjunct, similar to simplbi2 655. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Wolf Lammen, 10-Nov-2012.) |
Theorem | simpl2im 658 | Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021.) |
Theorem | simplbiim 659 | Implication from an eliminated conjunct equivalent to the antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | dfbi2 660 | A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 24-Jan-1993.) |
Theorem | dfbi 661 | Definition df-bi 197 rewritten in an abbreviated form to help intuitive understanding of that definition. Note that it is a conjunction of two implications; one which asserts properties that follow from the biconditional and one which asserts properties that imply the biconditional. (Contributed by NM, 15-Aug-2008.) |
Theorem | pm4.71 662 | Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 2-Dec-2012.) |
Theorem | pm4.71r 663 | Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 25-Jul-1999.) |
Theorem | pm4.71i 664 | Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.) |
Theorem | pm4.71ri 665 | Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.) |
Theorem | pm4.71d 666 | Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by Mario Carneiro, 25-Dec-2016.) |
Theorem | pm4.71rd 667 | Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.) |
Theorem | pm5.32 668 | Distribution of implication over biconditional. Theorem *5.32 of [WhiteheadRussell] p. 125. (Contributed by NM, 1-Aug-1994.) |
Theorem | pm5.32i 669 | Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.) |
Theorem | pm5.32ri 670 | Distribution of implication over biconditional (inference rule). (Contributed by NM, 12-Mar-1995.) |
Theorem | pm5.32d 671 | Distribution of implication over biconditional (deduction rule). (Contributed by NM, 29-Oct-1996.) |
Theorem | pm5.32rd 672 | Distribution of implication over biconditional (deduction rule). (Contributed by NM, 25-Dec-2004.) |
Theorem | pm5.32da 673 | Distribution of implication over biconditional (deduction rule). (Contributed by NM, 9-Dec-2006.) |
Theorem | biadan2 674 | Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) |
Theorem | pm4.24 675 | Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) |
Theorem | anidm 676 | Idempotent law for conjunction. (Contributed by NM, 8-Jan-2004.) (Proof shortened by Wolf Lammen, 14-Mar-2014.) |
Theorem | anidms 677 | Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.) |
Theorem | anidmdbi 678 | Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.) |
Theorem | anasss 679 | Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.) |
Theorem | anassrs 680 | Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.) |
Theorem | anass 681 | Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
Theorem | sylanl1 682 | A syllogism inference. (Contributed by NM, 10-Mar-2005.) |
Theorem | sylanl2 683 | A syllogism inference. (Contributed by NM, 1-Jan-2005.) |
Theorem | sylanr1 684 | A syllogism inference. (Contributed by NM, 9-Apr-2005.) |
Theorem | sylanr2 685 | A syllogism inference. (Contributed by NM, 9-Apr-2005.) |
Theorem | sylani 686 | A syllogism inference. (Contributed by NM, 2-May-1996.) |
Theorem | sylan2i 687 | A syllogism inference. (Contributed by NM, 1-Aug-1994.) |
Theorem | syl2ani 688 | A syllogism inference. (Contributed by NM, 3-Aug-1999.) |
Theorem | sylan9 689 | Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Theorem | sylan9r 690 | Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) |
Theorem | mtand 691 | A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.) |
Theorem | mtord 692 | A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.) |
Theorem | syl2anc 693 | Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.) |
Theorem | sylancl 694 | Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | sylancr 695 | Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | sylanblc 696 | Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.) |
Theorem | sylanblrc 697 | Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.) |
Theorem | sylanbrc 698 | Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | sylancb 699 | A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.) |
Theorem | sylancbr 700 | A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |