Home New Foundations ExplorerTheorem List (p. 7 of 64) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 601-700   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremexpl 601 Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)

Theoremimpr 602 Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)

Theoremimpl 603 Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)

Theoremimpac 604 Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994.)

Theoremexbiri 605 Inference form of exbir 1365. This proof is exbiriVD in set.mm automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.)

Theoremsimprbda 606 Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)

Theoremsimplbda 607 Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)

Theoremsimplbi2 608 Deduction eliminating a conjunct. Automatically derived from simplbi2VD in set.mm. (Contributed by Alan Sare, 31-Dec-2011.)

Theoremdfbi2 609 A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 5-Aug-1993.)

Theoremdfbi 610 Definition df-bi 177 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.)

Theorempm4.71 611 Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)

Theorempm4.71r 612 Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 25-Jul-1999.)

Theorempm4.71i 613 Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.)

Theorempm4.71ri 614 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.)

Theorempm4.71d 615 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.)

Theorempm4.71rd 616 Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.)

Theorempm5.32 617 Distribution of implication over biconditional. Theorem *5.32 of [WhiteheadRussell] p. 125. (Contributed by NM, 1-Aug-1994.)

Theorempm5.32i 618 Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.)

Theorempm5.32ri 619 Distribution of implication over biconditional (inference rule). (Contributed by NM, 12-Mar-1995.)

Theorempm5.32d 620 Distribution of implication over biconditional (deduction rule). (Contributed by NM, 29-Oct-1996.)

Theorempm5.32rd 621 Distribution of implication over biconditional (deduction rule). (Contributed by NM, 25-Dec-2004.)

Theorempm5.32da 622 Distribution of implication over biconditional (deduction rule). (Contributed by NM, 9-Dec-2006.)

Theorempm4.24 624 Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)

Theoremanidm 625 Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)

Theoremanidms 626 Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)

Theoremanidmdbi 627 Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.)

Theoremanasss 628 Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)

Theoremanassrs 629 Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)

Theoremanass 630 Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Theoremsylanl1 631 A syllogism inference. (Contributed by NM, 10-Mar-2005.)

Theoremsylanl2 632 A syllogism inference. (Contributed by NM, 1-Jan-2005.)

Theoremsylanr1 633 A syllogism inference. (Contributed by NM, 9-Apr-2005.)

Theoremsylanr2 634 A syllogism inference. (Contributed by NM, 9-Apr-2005.)

Theoremsylani 635 A syllogism inference. (Contributed by NM, 2-May-1996.)

Theoremsylan2i 636 A syllogism inference. (Contributed by NM, 1-Aug-1994.)

Theoremsyl2ani 637 A syllogism inference. (Contributed by NM, 3-Aug-1999.)

Theoremsylan9 638 Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Theoremsylan9r 639 Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.)

Theoremmtand 640 A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)

Theoremmtord 641 A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.)

Theoremsyl2anc 642 Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)

Theoremsylancl 643 Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Theoremsylancr 644 Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Theoremsylanbrc 645 Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)

Theoremsylancb 646 A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)

Theoremsylancbr 647 A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)

Theoremsylancom 648 Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008.)

Theoremmpdan 649 An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Theoremmpancom 650 An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Theoremmpan 651 An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Theoremmpan2 652 An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Theoremmp2an 653 An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)

Theoremmp4an 654 An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.)

Theoremmpan2d 655 A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)

Theoremmpand 656 A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Theoremmpani 657 An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Theoremmpan2i 658 An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Theoremmp2ani 659 An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.)

Theoremmp2and 660 A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)

Theoremmpanl1 661 An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Theoremmpanl2 662 An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Theoremmpanl12 663 An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)

Theoremmpanr1 664 An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Theoremmpanr2 665 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.)

Theoremmpanr12 666 An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)

Theoremmpanlr1 667 An inference based on modus ponens. (Contributed by NM, 30-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Theorempm5.74da 668 Distribution of implication over biconditional (deduction rule). (Contributed by NM, 4-May-2007.)

Theorempm4.45 669 Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)

Theoremimdistan 670 Distribution of implication with conjunction. (Contributed by NM, 31-May-1999.) (Proof shortened by Wolf Lammen, 6-Dec-2012.)

Theoremimdistani 671 Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)

Theoremimdistanri 672 Distribution of implication with conjunction. (Contributed by NM, 8-Jan-2002.)

Theoremimdistand 673 Distribution of implication with conjunction (deduction rule). (Contributed by NM, 27-Aug-2004.)

Theoremimdistanda 674 Distribution of implication with conjunction (deduction version with conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.)

Theoremanbi2i 675 Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Theoremanbi1i 676 Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Theoremanbi2ci 677 Variant of anbi2i 675 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)

Theoremanbi12i 678 Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.)

Theoremanbi12ci 679 Variant of anbi12i 678 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Theoremsylan9bb 680 Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)

Theoremsylan9bbr 681 Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)

Theoremorbi2d 682 Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Theoremorbi1d 683 Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Theoremanbi2d 684 Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Theoremanbi1d 685 Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Theoremorbi1 686 Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)

Theoremanbi1 687 Introduce a right conjunct to both sides of a logical equivalence. Theorem *4.36 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)

Theoremanbi2 688 Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 16-Nov-2013.)

Theorembitr 689 Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)

Theoremorbi12d 690 Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)

Theoremanbi12d 691 Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 5-Aug-1993.)

Theorempm5.3 692 Theorem *5.3 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Theorempm5.61 693 Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.)

Theoremadantll 694 Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Theoremadantlr 695 Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Theoremadantrl 696 Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Theoremadantrr 697 Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Theoremadantlll 698 Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)

Theoremadantllr 699 Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Theoremadantlrl 700 Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6338
 Copyright terms: Public domain < Previous  Next >