HomeTheorem List (p. 7 of 411)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 7 of 411) | < 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-26652) |
Hilbert Space Explorer
(26653-28175) |
Users' Mathboxes
(28176-41046) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | imp4b 601 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
      
   ![/\](wedge.gif "/\"){kind=small} | ||
| Theorem | imp4c 602 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp4d 603 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp41 604 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp42 605 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp43 606 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp44 607 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp45 608 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp5a 609 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
 | ||
| Theorem | imp5d 610 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
|
| ||
| Theorem | imp5g 611 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
|
| ||
| Theorem | imp55 612 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
|
| ||
| Theorem | imp511 613 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
|
| ||
| Theorem | expimpd 614 | Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.) |
| | ||
| Theorem | exp31 615 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
| | ||
| Theorem | exp32 616 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
| | ||
| Theorem | exp4a 617 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | exp4b 618 | An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) |
|
| ||
| Theorem | exp4c 619 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | exp4d 620 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | exp41 621 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | exp42 622 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | exp43 623 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | exp44 624 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | exp45 625 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | expr 626 | Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.) |
| | ||
| Theorem | exp5c 627 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
|
| ||
| Theorem | exp5j 628 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
|
| ||
| Theorem | exp53 629 | An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.) |
|
| ||
| Theorem | expl 630 | Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.) |
| | ||
| Theorem | impr 631 | Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.) |
| | ||
| Theorem | impl 632 | Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.) |
|
| ||
| Theorem | impac 633 | Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994.) |
| | ||
| Theorem | exbiri 634 | Inference form of exbir 36903. This proof is exbiriVD 37313 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.) |
| ||
| Theorem | simprbda 635 | Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.) |
| | ||
| Theorem | simplbda 636 | Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.) |
| | ||
| Theorem | simplbi2 637 | Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.) |
| | ||
| Theorem | simplbi2comt 638 | Closed form of simplbi2com 639. (Contributed by Alan Sare, 22-Jul-2012.) |
| | ||
| Theorem | simplbi2com 639 | A deduction eliminating a conjunct, similar to simplbi2 637. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Wolf Lammen, 10-Nov-2012.) |
| | ||
| Theorem | dfbi2 640 | A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 24-Jan-1993.) |
| | ||
| Theorem | dfbi 641 | Definition df-bi 190 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 642 | 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 643 | 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 644 | 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 645 | 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 646 | 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 647 | 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 648 | Distribution of implication over biconditional. Theorem *5.32 of [WhiteheadRussell] p. 125. (Contributed by NM, 1-Aug-1994.) |
| | ||
| Theorem | pm5.32i 649 | Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.) |
| | ||
| Theorem | pm5.32ri 650 | Distribution of implication over biconditional (inference rule). (Contributed by NM, 12-Mar-1995.) |
| | ||
| Theorem | pm5.32d 651 | Distribution of implication over biconditional (deduction rule). (Contributed by NM, 29-Oct-1996.) |
|
| ||
| Theorem | pm5.32rd 652 | Distribution of implication over biconditional (deduction rule). (Contributed by NM, 25-Dec-2004.) |
|
| ||
| Theorem | pm5.32da 653 | Distribution of implication over biconditional (deduction rule). (Contributed by NM, 9-Dec-2006.) |
| | ||
| Theorem | biadan2 654 | Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) |
 | ||
| Theorem | pm4.24 655 | Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) |
| | ||
| Theorem | anidm 656 | Idempotent law for conjunction. (Contributed by NM, 8-Jan-2004.) (Proof shortened by Wolf Lammen, 14-Mar-2014.) |
| | ||
| Theorem | anidms 657 | Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.) |
| | ||
| Theorem | anidmdbi 658 | Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.) |
| | ||
| Theorem | anasss 659 | Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.) |
| | ||
| Theorem | anassrs 660 | Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.) |
| | ||
| Theorem | anass 661 | 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 662 | A syllogism inference. (Contributed by NM, 10-Mar-2005.) |
| | ||
| Theorem | sylanl2 663 | A syllogism inference. (Contributed by NM, 1-Jan-2005.) |
| | ||
| Theorem | sylanr1 664 | A syllogism inference. (Contributed by NM, 9-Apr-2005.) |
|
| ||
| Theorem | sylanr2 665 | A syllogism inference. (Contributed by NM, 9-Apr-2005.) |
|
| ||
| Theorem | sylani 666 | A syllogism inference. (Contributed by NM, 2-May-1996.) |
|
| ||
| Theorem | sylan2i 667 | A syllogism inference. (Contributed by NM, 1-Aug-1994.) |
| | ||
| Theorem | syl2ani 668 | A syllogism inference. (Contributed by NM, 3-Aug-1999.) |
| | ||
| Theorem | sylan9 669 | Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
| | ||
| Theorem | sylan9r 670 | Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) |
|
| ||
| Theorem | mtand 671 | A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.) |
 | ||
| Theorem | mtord 672 | A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.) |
 | ||
| Theorem | syl2anc 673 | Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.) |
| | ||
| Theorem | hypstkdOLD 674 | Obsolete proof of mpidan 683 as of 28-Mar-2021. (Contributed by Stanislas Polu, 9-Mar-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
| | ||
| Theorem | sylancl 675 | Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| | ||
| Theorem | sylancr 676 | Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| | ||
| Theorem | sylanbrc 677 | Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| | ||
| Theorem | sylancb 678 | A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.) |
| | ||
| Theorem | sylancbr 679 | A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.) |
| | ||
| Theorem | sylancom 680 | Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008.) |
|
| ||
| Theorem | mpdan 681 | An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.) |
|
| ||
| Theorem | mpancom 682 | An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
|
| ||
| Theorem | mpidan 683 | A deduction which "stacks" a hypothesis. (Contributed by Stanislas Polu, 9-Mar-2020.) (Proof shortened by Wolf Lammen, 28-Mar-2021.) |
| | ||
| Theorem | mpan 684 | An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
| | ||
| Theorem | mpan2 685 | An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.) |
| | ||
| Theorem | mp2an 686 | An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.) |
| | ||
| Theorem | mp4an 687 | An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.) |
| | ||
| Theorem | mpan2d 688 | A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) |
| | ||
| Theorem | mpand 689 | A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
| | ||
| Theorem | mpani 690 | An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.) |
|
| ||
| Theorem | mpan2i 691 | An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.) |
|
| ||
| Theorem | mp2ani 692 | An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.) |
| | ||
| Theorem | mp2and 693 | A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) |
| | ||
| Theorem | mpanl1 694 | An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
|
| ||
| Theorem | mpanl2 695 | An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
| | ||
| Theorem | mpanl12 696 | An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.) |
| | ||
| Theorem | mpanr1 697 | An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
| | ||
| Theorem | mpanr2 698 | An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
| | ||
| Theorem | mpanr12 699 | An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.) |
| | ||
| Theorem | mpanlr1 700 | An inference based on modus ponens. (Contributed by NM, 30-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |