 Home New Foundations ExplorerTheorem List (p. 7 of 64) < Previous  Next > Bad symbols? Try the GIF 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-6336
 Copyright terms: Public domain < Previous  Next >