HomeHome New Foundations Explorer
Theorem List (p. 8 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 - 701-800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremadantlrr 701 Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
(((φ ψ) χ) → θ)       (((φ (ψ τ)) χ) → θ)
 
Theoremadantrll 702 Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
((φ (ψ χ)) → θ)       ((φ ((τ ψ) χ)) → θ)
 
Theoremadantrlr 703 Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
((φ (ψ χ)) → θ)       ((φ ((ψ τ) χ)) → θ)
 
Theoremadantrrl 704 Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
((φ (ψ χ)) → θ)       ((φ (ψ (τ χ))) → θ)
 
Theoremadantrrr 705 Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
((φ (ψ χ)) → θ)       ((φ (ψ (χ τ))) → θ)
 
Theoremad2antrr 706 Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
(φψ)       (((φ χ) θ) → ψ)
 
Theoremad2antlr 707 Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
(φψ)       (((χ φ) θ) → ψ)
 
Theoremad2antrl 708 Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
(φψ)       ((χ (φ θ)) → ψ)
 
Theoremad2antll 709 Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
(φψ)       ((χ (θ φ)) → ψ)
 
Theoremad3antrrr 710 Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)
(φψ)       ((((φ χ) θ) τ) → ψ)
 
Theoremad3antlr 711 Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
(φψ)       ((((χ φ) θ) τ) → ψ)
 
Theoremad4antr 712 Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
(φψ)       (((((φ χ) θ) τ) η) → ψ)
 
Theoremad4antlr 713 Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
(φψ)       (((((χ φ) θ) τ) η) → ψ)
 
Theoremad5antr 714 Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
(φψ)       ((((((φ χ) θ) τ) η) ζ) → ψ)
 
Theoremad5antlr 715 Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
(φψ)       ((((((χ φ) θ) τ) η) ζ) → ψ)
 
Theoremad6antr 716 Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
(φψ)       (((((((φ χ) θ) τ) η) ζ) σ) → ψ)
 
Theoremad6antlr 717 Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
(φψ)       (((((((χ φ) θ) τ) η) ζ) σ) → ψ)
 
Theoremad7antr 718 Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
(φψ)       ((((((((φ χ) θ) τ) η) ζ) σ) ρ) → ψ)
 
Theoremad7antlr 719 Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
(φψ)       ((((((((χ φ) θ) τ) η) ζ) σ) ρ) → ψ)
 
Theoremad8antr 720 Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
(φψ)       (((((((((φ χ) θ) τ) η) ζ) σ) ρ) μ) → ψ)
 
Theoremad8antlr 721 Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
(φψ)       (((((((((χ φ) θ) τ) η) ζ) σ) ρ) μ) → ψ)
 
Theoremad9antr 722 Deduction adding 9 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
(φψ)       ((((((((((φ χ) θ) τ) η) ζ) σ) ρ) μ) λ) → ψ)
 
Theoremad9antlr 723 Deduction adding 9 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
(φψ)       ((((((((((χ φ) θ) τ) η) ζ) σ) ρ) μ) λ) → ψ)
 
Theoremad10antr 724 Deduction adding 10 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
(φψ)       (((((((((((φ χ) θ) τ) η) ζ) σ) ρ) μ) λ) κ) → ψ)
 
Theoremad10antlr 725 Deduction adding 10 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
(φψ)       (((((((((((χ φ) θ) τ) η) ζ) σ) ρ) μ) λ) κ) → ψ)
 
Theoremad2ant2l 726 Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
((φ ψ) → χ)       (((θ φ) (τ ψ)) → χ)
 
Theoremad2ant2r 727 Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
((φ ψ) → χ)       (((φ θ) (ψ τ)) → χ)
 
Theoremad2ant2lr 728 Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)
((φ ψ) → χ)       (((θ φ) (ψ τ)) → χ)
 
Theoremad2ant2rl 729 Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)
((φ ψ) → χ)       (((φ θ) (τ ψ)) → χ)
 
Theoremsimpll 730 Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
(((φ ψ) χ) → φ)
 
Theoremsimplr 731 Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)
(((φ ψ) χ) → ψ)
 
Theoremsimprl 732 Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
((φ (ψ χ)) → ψ)
 
Theoremsimprr 733 Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
((φ (ψ χ)) → χ)
 
Theoremsimplll 734 Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
((((φ ψ) χ) θ) → φ)
 
Theoremsimpllr 735 Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
((((φ ψ) χ) θ) → ψ)
 
Theoremsimplrl 736 Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
(((φ (ψ χ)) θ) → ψ)
 
Theoremsimplrr 737 Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
(((φ (ψ χ)) θ) → χ)
 
Theoremsimprll 738 Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
((φ ((ψ χ) θ)) → ψ)
 
Theoremsimprlr 739 Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
((φ ((ψ χ) θ)) → χ)
 
Theoremsimprrl 740 Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
((φ (ψ (χ θ))) → χ)
 
Theoremsimprrr 741 Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
((φ (ψ (χ θ))) → θ)
 
Theoremsimp-4l 742 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
(((((φ ψ) χ) θ) τ) → φ)
 
Theoremsimp-4r 743 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
(((((φ ψ) χ) θ) τ) → ψ)
 
Theoremsimp-5l 744 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
((((((φ ψ) χ) θ) τ) η) → φ)
 
Theoremsimp-5r 745 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
((((((φ ψ) χ) θ) τ) η) → ψ)
 
Theoremsimp-6l 746 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
(((((((φ ψ) χ) θ) τ) η) ζ) → φ)
 
Theoremsimp-6r 747 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
(((((((φ ψ) χ) θ) τ) η) ζ) → ψ)
 
Theoremsimp-7l 748 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
((((((((φ ψ) χ) θ) τ) η) ζ) σ) → φ)
 
Theoremsimp-7r 749 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
((((((((φ ψ) χ) θ) τ) η) ζ) σ) → ψ)
 
Theoremsimp-8l 750 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
(((((((((φ ψ) χ) θ) τ) η) ζ) σ) ρ) → φ)
 
Theoremsimp-8r 751 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
(((((((((φ ψ) χ) θ) τ) η) ζ) σ) ρ) → ψ)
 
Theoremsimp-9l 752 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
((((((((((φ ψ) χ) θ) τ) η) ζ) σ) ρ) μ) → φ)
 
Theoremsimp-9r 753 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
((((((((((φ ψ) χ) θ) τ) η) ζ) σ) ρ) μ) → ψ)
 
Theoremsimp-10l 754 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
(((((((((((φ ψ) χ) θ) τ) η) ζ) σ) ρ) μ) λ) → φ)
 
Theoremsimp-10r 755 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
(((((((((((φ ψ) χ) θ) τ) η) ζ) σ) ρ) μ) λ) → ψ)
 
Theoremsimp-11l 756 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
((((((((((((φ ψ) χ) θ) τ) η) ζ) σ) ρ) μ) λ) κ) → φ)
 
Theoremsimp-11r 757 Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
((((((((((((φ ψ) χ) θ) τ) η) ζ) σ) ρ) μ) λ) κ) → ψ)
 
Theoremjaob 758 Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
(((φ χ) → ψ) ↔ ((φψ) (χψ)))
 
Theoremjaoian 759 Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.)
((φ ψ) → χ)    &   ((θ ψ) → χ)       (((φ θ) ψ) → χ)
 
Theoremjaodan 760 Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)
((φ ψ) → χ)    &   ((φ θ) → χ)       ((φ (ψ θ)) → χ)
 
Theoremmpjaodan 761 Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination), see natded in set.mm. (Contributed by Mario Carneiro, 29-May-2016.)
((φ ψ) → χ)    &   ((φ θ) → χ)    &   (φ → (ψ θ))       (φχ)
 
Theorempm4.77 762 Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
(((ψφ) (χφ)) ↔ ((ψ χ) → φ))
 
Theorempm2.63 763 Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
((φ ψ) → ((¬ φ ψ) → ψ))
 
Theorempm2.64 764 Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
((φ ψ) → ((φ ¬ ψ) → φ))
 
Theorempm2.61ian 765 Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
((φ ψ) → χ)    &   ((¬ φ ψ) → χ)       (ψχ)
 
Theorempm2.61dan 766 Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
((φ ψ) → χ)    &   ((φ ¬ ψ) → χ)       (φχ)
 
Theorempm2.61ddan 767 Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.)
((φ ψ) → θ)    &   ((φ χ) → θ)    &   ((φ ψ ¬ χ)) → θ)       (φθ)
 
Theorempm2.61dda 768 Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.)
((φ ¬ ψ) → θ)    &   ((φ ¬ χ) → θ)    &   ((φ (ψ χ)) → θ)       (φθ)
 
Theoremcondan 769 Proof by contradiction. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Wolf Lammen, 19-Jun-2014.)
((φ ¬ ψ) → χ)    &   ((φ ¬ ψ) → ¬ χ)       (φψ)
 
Theoremabai 770 Introduce one conjunct as an antecedent to the other. "abai" stands for "and, biconditional, and, implication". (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)
((φ ψ) ↔ (φ (φψ)))
 
Theorempm5.53 771 Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
((((φ ψ) χ) → θ) ↔ (((φθ) (ψθ)) (χθ)))
 
Theoreman12 772 Swap two conjuncts. Note that the first digit (1) in the label refers to the outer conjunct position, and the next digit (2) to the inner conjunct position. (Contributed by NM, 12-Mar-1995.)
((φ (ψ χ)) ↔ (ψ (φ χ)))
 
Theoreman32 773 A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
(((φ ψ) χ) ↔ ((φ χ) ψ))
 
Theoreman13 774 A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
((φ (ψ χ)) ↔ (χ (ψ φ)))
 
Theoreman31 775 A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
(((φ ψ) χ) ↔ ((χ ψ) φ))
 
Theoreman12s 776 Swap two conjuncts in antecedent. The label suffix "s" means that an12 772 is combined with syl 15 (or a variant). (Contributed by NM, 13-Mar-1996.)
((φ (ψ χ)) → θ)       ((ψ (φ χ)) → θ)
 
Theoremancom2s 777 Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
((φ (ψ χ)) → θ)       ((φ (χ ψ)) → θ)
 
Theoreman13s 778 Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
((φ (ψ χ)) → θ)       ((χ (ψ φ)) → θ)
 
Theoreman32s 779 Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
(((φ ψ) χ) → θ)       (((φ χ) ψ) → θ)
 
Theoremancom1s 780 Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
(((φ ψ) χ) → θ)       (((ψ φ) χ) → θ)
 
Theoreman31s 781 Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
(((φ ψ) χ) → θ)       (((χ ψ) φ) → θ)
 
Theoremanass1rs 782 Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.)
((φ (ψ χ)) → θ)       (((φ χ) ψ) → θ)
 
Theoremanabs1 783 Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
(((φ ψ) φ) ↔ (φ ψ))
 
Theoremanabs5 784 Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
((φ (φ ψ)) ↔ (φ ψ))
 
Theoremanabs7 785 Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 17-Nov-2013.)
((ψ (φ ψ)) ↔ (φ ψ))
 
Theoremanabsan 786 Absorption of antecedent with conjunction. (Contributed by NM, 24-Mar-1996.)
(((φ φ) ψ) → χ)       ((φ ψ) → χ)
 
Theoremanabss1 787 Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
(((φ ψ) φ) → χ)       ((φ ψ) → χ)
 
Theoremanabss4 788 Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.)
(((ψ φ) ψ) → χ)       ((φ ψ) → χ)
 
Theoremanabss5 789 Absorption of antecedent into conjunction. (Contributed by NM, 10-May-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
((φ (φ ψ)) → χ)       ((φ ψ) → χ)
 
Theoremanabsi5 790 Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
(φ → ((φ ψ) → χ))       ((φ ψ) → χ)
 
Theoremanabsi6 791 Absorption of antecedent into conjunction. (Contributed by NM, 14-Aug-2000.)
(φ → ((ψ φ) → χ))       ((φ ψ) → χ)
 
Theoremanabsi7 792 Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
(ψ → ((φ ψ) → χ))       ((φ ψ) → χ)
 
Theoremanabsi8 793 Absorption of antecedent into conjunction. (Contributed by NM, 26-Sep-1999.)
(ψ → ((ψ φ) → χ))       ((φ ψ) → χ)
 
Theoremanabss7 794 Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 19-Nov-2013.)
((ψ (φ ψ)) → χ)       ((φ ψ) → χ)
 
Theoremanabsan2 795 Absorption of antecedent with conjunction. (Contributed by NM, 10-May-2004.)
((φ (ψ ψ)) → χ)       ((φ ψ) → χ)
 
Theoremanabss3 796 Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
(((φ ψ) ψ) → χ)       ((φ ψ) → χ)
 
Theoreman4 797 Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
(((φ ψ) (χ θ)) ↔ ((φ χ) (ψ θ)))
 
Theoreman42 798 Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
(((φ ψ) (χ θ)) ↔ ((φ χ) (θ ψ)))
 
Theoreman4s 799 Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
(((φ ψ) (χ θ)) → τ)       (((φ χ) (ψ θ)) → τ)
 
Theoreman42s 800 Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
(((φ ψ) (χ θ)) → τ)       (((φ χ) (θ ψ)) → τ)
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700701-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-6329
  Copyright terms: Public domain < Previous  Next >