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