HomeHome New Foundations Explorer
Theorem List (p. 10 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 - 901-1000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorembigolden 901 Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
(((φ ψ) ↔ φ) ↔ (ψ ↔ (φ ψ)))
 
Theorempm5.71 902 Theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.)
((ψ → ¬ χ) → (((φ ψ) χ) ↔ (φ χ)))
 
Theorempm5.75 903 Theorem *5.75 of [WhiteheadRussell] p. 126. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2012.)
(((χ → ¬ ψ) (φ ↔ (ψ χ))) → ((φ ¬ ψ) ↔ χ))
 
Theorembimsc1 904 Removal of conjunct from one side of an equivalence. (Contributed by NM, 5-Aug-1993.)
(((φψ) (χ ↔ (ψ φ))) → (χφ))
 
Theorem4exmid 905 The disjunction of the four possible combinations of two wffs and their negations is always true. (Contributed by David Abernethy, 28-Jan-2014.)
(((φ ψ) φ ¬ ψ)) ((φ ¬ ψ) (ψ ¬ φ)))
 
Theoremecase2d 906 Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Dec-2012.)
(φψ)    &   (φ → ¬ (ψ χ))    &   (φ → ¬ (ψ θ))    &   (φ → (τ (χ θ)))       (φτ)
 
Theoremecase3 907 Inference for elimination by cases. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
(φχ)    &   (ψχ)    &   (¬ (φ ψ) → χ)       χ
 
Theoremecase 908 Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.)
φχ)    &   ψχ)    &   ((φ ψ) → χ)       χ
 
Theoremecase3d 909 Deduction for elimination by cases. (Contributed by NM, 2-May-1996.) (Proof shortened by Andrew Salmon, 7-May-2011.)
(φ → (ψθ))    &   (φ → (χθ))    &   (φ → (¬ (ψ χ) → θ))       (φθ)
 
Theoremecased 910 Deduction for elimination by cases. (Contributed by NM, 8-Oct-2012.)
(φ → (¬ ψθ))    &   (φ → (¬ χθ))    &   (φ → ((ψ χ) → θ))       (φθ)
 
Theoremecase3ad 911 Deduction for elimination by cases. (Contributed by NM, 24-May-2013.)
(φ → (ψθ))    &   (φ → (χθ))    &   (φ → ((¬ ψ ¬ χ) → θ))       (φθ)
 
Theoremccase 912 Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
((φ ψ) → τ)    &   ((χ ψ) → τ)    &   ((φ θ) → τ)    &   ((χ θ) → τ)       (((φ χ) (ψ θ)) → τ)
 
Theoremccased 913 Deduction for combining cases. (Contributed by NM, 9-May-2004.)
(φ → ((ψ χ) → η))    &   (φ → ((θ χ) → η))    &   (φ → ((ψ τ) → η))    &   (φ → ((θ τ) → η))       (φ → (((ψ θ) (χ τ)) → η))
 
Theoremccase2 914 Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
((φ ψ) → τ)    &   (χτ)    &   (θτ)       (((φ χ) (ψ θ)) → τ)
 
Theorem4cases 915 Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 25-Oct-2003.)
((φ ψ) → χ)    &   ((φ ¬ ψ) → χ)    &   ((¬ φ ψ) → χ)    &   ((¬ φ ¬ ψ) → χ)       χ
 
Theorem4casesdan 916 Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 19-Mar-2013.)
((φ (ψ χ)) → θ)    &   ((φ (ψ ¬ χ)) → θ)    &   ((φ ψ χ)) → θ)    &   ((φ ψ ¬ χ)) → θ)       (φθ)
 
Theoremniabn 917 Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
φ       ψ → ((χ ψ) ↔ ¬ φ))
 
Theoremdedlem0a 918 Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
(φ → (ψ ↔ ((χφ) → (ψ φ))))
 
Theoremdedlem0b 919 Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.)
φ → (ψ ↔ ((ψφ) → (χ φ))))
 
Theoremdedlema 920 Lemma for weak deduction theorem. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.)
(φ → (ψ ↔ ((ψ φ) (χ ¬ φ))))
 
Theoremdedlemb 921 Lemma for weak deduction theorem. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.)
φ → (χ ↔ ((ψ φ) (χ ¬ φ))))
 
Theoremelimh 922 Hypothesis builder for weak deduction theorem. For more information, see the Deduction Theorem link on the Metamath Proof Explorer home page. (Contributed by NM, 26-Jun-2002.)
((φ ↔ ((φ χ) (ψ ¬ χ))) → (χτ))    &   ((ψ ↔ ((φ χ) (ψ ¬ χ))) → (θτ))    &   θ       τ
 
Theoremdedt 923 The weak deduction theorem. For more information, see the Deduction Theorem link on the Metamath Proof Explorer home page. (Contributed by NM, 26-Jun-2002.)
((φ ↔ ((φ χ) (ψ ¬ χ))) → (θτ))    &   τ       (χθ)
 
Theoremcon3th 924 Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. This version of con3 126 demonstrates the use of the weak deduction theorem dedt 923 to derive it from con3i 127. (Contributed by NM, 27-Jun-2002.) (Proof modification is discouraged.)
((φψ) → (¬ ψ → ¬ φ))
 
Theoremconsensus 925 The consensus theorem. This theorem and its dual (with and interchanged) are commonly used in computer logic design to eliminate redundant terms from Boolean expressions. Specifically, we prove that the term (ψ χ) on the left-hand side is redundant. (Contributed by NM, 16-May-2003.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 20-Jan-2013.)
((((φ ψ) φ χ)) (ψ χ)) ↔ ((φ ψ) φ χ)))
 
Theorempm4.42 926 Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed by Roy F. Longton, 21-Jun-2005.)
(φ ↔ ((φ ψ) (φ ¬ ψ)))
 
Theoremninba 927 Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
φ       ψ → (¬ φ ↔ (χ ψ)))
 
Theoremprlem1 928 A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
(φ → (ηχ))    &   (ψ → ¬ θ)       (φ → (ψ → (((ψ χ) (θ τ)) → η)))
 
Theoremprlem2 929 A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
(((φ ψ) (χ θ)) ↔ ((φ χ) ((φ ψ) (χ θ))))
 
Theoremoplem1 930 A specialized lemma for set theory (ordered pair theorem). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Wolf Lammen, 8-Dec-2012.)
(φ → (ψ χ))    &   (φ → (θ τ))    &   (ψθ)    &   (χ → (θτ))       (φψ)
 
Theoremrnlem 931 Lemma used in construction of real numbers. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
(((φ ψ) (χ θ)) ↔ (((φ χ) (ψ θ)) ((φ θ) (ψ χ))))
 
Theoremdn1 932 A single axiom for Boolean algebra known as DN1. See http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf. (Contributed by Jeffrey Hankins, 3-Jul-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
(¬ (¬ (¬ (φ ψ) χ) ¬ (φ ¬ (¬ χ ¬ (χ θ)))) ↔ χ)
 
1.2.8  Abbreviated conjunction and disjunction of three wff's
 
Syntaxw3o 933 Extend wff definition to include 3-way disjunction ('or').
wff (φ ψ χ)
 
Syntaxw3a 934 Extend wff definition to include 3-way conjunction ('and').
wff (φ ψ χ)
 
Definitiondf-3or 935 Define disjunction ('or') of three wff's. Definition *2.33 of [WhiteheadRussell] p. 105. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law orass 510. (Contributed by NM, 8-Apr-1994.)
((φ ψ χ) ↔ ((φ ψ) χ))
 
Definitiondf-3an 936 Define conjunction ('and') of three wff's. Definition *4.34 of [WhiteheadRussell] p. 118. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law anass 630. (Contributed by NM, 8-Apr-1994.)
((φ ψ χ) ↔ ((φ ψ) χ))
 
Theorem3orass 937 Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
((φ ψ χ) ↔ (φ (ψ χ)))
 
Theorem3anass 938 Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
((φ ψ χ) ↔ (φ (ψ χ)))
 
Theorem3anrot 939 Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
((φ ψ χ) ↔ (ψ χ φ))
 
Theorem3orrot 940 Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
((φ ψ χ) ↔ (ψ χ φ))
 
Theorem3ancoma 941 Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
((φ ψ χ) ↔ (ψ φ χ))
 
Theorem3orcoma 942 Commutation law for triple disjunction. (Contributed by Mario Carneiro, 4-Sep-2016.)
((φ ψ χ) ↔ (ψ φ χ))
 
Theorem3ancomb 943 Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
((φ ψ χ) ↔ (φ χ ψ))
 
Theorem3orcomb 944 Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.)
((φ ψ χ) ↔ (φ χ ψ))
 
Theorem3anrev 945 Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
((φ ψ χ) ↔ (χ ψ φ))
 
Theorem3anan32 946 Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
((φ ψ χ) ↔ ((φ χ) ψ))
 
Theorem3anan12 947 Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
((φ ψ χ) ↔ (ψ (φ χ)))
 
Theorem3anor 948 Triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.)
((φ ψ χ) ↔ ¬ (¬ φ ¬ ψ ¬ χ))
 
Theorem3ianor 949 Negated triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.)
(¬ (φ ψ χ) ↔ (¬ φ ¬ ψ ¬ χ))
 
Theorem3ioran 950 Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)
(¬ (φ ψ χ) ↔ (¬ φ ¬ ψ ¬ χ))
 
Theorem3oran 951 Triple disjunction in terms of triple conjunction. (Contributed by NM, 8-Oct-2012.)
((φ ψ χ) ↔ ¬ (¬ φ ¬ ψ ¬ χ))
 
Theorem3simpa 952 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
((φ ψ χ) → (φ ψ))
 
Theorem3simpb 953 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
((φ ψ χ) → (φ χ))
 
Theorem3simpc 954 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)
((φ ψ χ) → (ψ χ))
 
Theoremsimp1 955 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
((φ ψ χ) → φ)
 
Theoremsimp2 956 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
((φ ψ χ) → ψ)
 
Theoremsimp3 957 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
((φ ψ χ) → χ)
 
Theoremsimpl1 958 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
(((φ ψ χ) θ) → φ)
 
Theoremsimpl2 959 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
(((φ ψ χ) θ) → ψ)
 
Theoremsimpl3 960 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
(((φ ψ χ) θ) → χ)
 
Theoremsimpr1 961 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
((φ (ψ χ θ)) → ψ)
 
Theoremsimpr2 962 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
((φ (ψ χ θ)) → χ)
 
Theoremsimpr3 963 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
((φ (ψ χ θ)) → θ)
 
Theoremsimp1i 964 Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
(φ ψ χ)       φ
 
Theoremsimp2i 965 Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
(φ ψ χ)       ψ
 
Theoremsimp3i 966 Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
(φ ψ χ)       χ
 
Theoremsimp1d 967 Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
(φ → (ψ χ θ))       (φψ)
 
Theoremsimp2d 968 Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
(φ → (ψ χ θ))       (φχ)
 
Theoremsimp3d 969 Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
(φ → (ψ χ θ))       (φθ)
 
Theoremsimp1bi 970 Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(φ ↔ (ψ χ θ))       (φψ)
 
Theoremsimp2bi 971 Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(φ ↔ (ψ χ θ))       (φχ)
 
Theoremsimp3bi 972 Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(φ ↔ (ψ χ θ))       (φθ)
 
Theorem3adant1 973 Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
((φ ψ) → χ)       ((θ φ ψ) → χ)
 
Theorem3adant2 974 Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
((φ ψ) → χ)       ((φ θ ψ) → χ)
 
Theorem3adant3 975 Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
((φ ψ) → χ)       ((φ ψ θ) → χ)
 
Theorem3ad2ant1 976 Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
(φχ)       ((φ ψ θ) → χ)
 
Theorem3ad2ant2 977 Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
(φχ)       ((ψ φ θ) → χ)
 
Theorem3ad2ant3 978 Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
(φχ)       ((ψ θ φ) → χ)
 
Theoremsimp1l 979 Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
(((φ ψ) χ θ) → φ)
 
Theoremsimp1r 980 Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
(((φ ψ) χ θ) → ψ)
 
Theoremsimp2l 981 Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
((φ (ψ χ) θ) → ψ)
 
Theoremsimp2r 982 Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
((φ (ψ χ) θ) → χ)
 
Theoremsimp3l 983 Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
((φ ψ (χ θ)) → χ)
 
Theoremsimp3r 984 Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
((φ ψ (χ θ)) → θ)
 
Theoremsimp11 985 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
(((φ ψ χ) θ τ) → φ)
 
Theoremsimp12 986 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
(((φ ψ χ) θ τ) → ψ)
 
Theoremsimp13 987 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
(((φ ψ χ) θ τ) → χ)
 
Theoremsimp21 988 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
((φ (ψ χ θ) τ) → ψ)
 
Theoremsimp22 989 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
((φ (ψ χ θ) τ) → χ)
 
Theoremsimp23 990 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
((φ (ψ χ θ) τ) → θ)
 
Theoremsimp31 991 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
((φ ψ (χ θ τ)) → χ)
 
Theoremsimp32 992 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
((φ ψ (χ θ τ)) → θ)
 
Theoremsimp33 993 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
((φ ψ (χ θ τ)) → τ)
 
Theoremsimpll1 994 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
((((φ ψ χ) θ) τ) → φ)
 
Theoremsimpll2 995 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
((((φ ψ χ) θ) τ) → ψ)
 
Theoremsimpll3 996 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
((((φ ψ χ) θ) τ) → χ)
 
Theoremsimplr1 997 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
(((θ (φ ψ χ)) τ) → φ)
 
Theoremsimplr2 998 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
(((θ (φ ψ χ)) τ) → ψ)
 
Theoremsimplr3 999 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
(((θ (φ ψ χ)) τ) → χ)
 
Theoremsimprl1 1000 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
((τ ((φ ψ χ) θ)) → φ)
    < 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-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 >