HomeHome Intuitionistic Logic Explorer
Theorem List (p. 10 of 20)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 901-1000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdn1 901 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.) (The proof was shortened by Andrew Salmon, 13-May-2011.) (The proof was shortened by Wolf Lammen, 6-Jan-2013.)
 
1.2.9  Abbreviated conjunction and disjunction of three wff's
 
Syntaxw3o 902 Extend wff definition to include 3-way disjunction ('or').
 
Syntaxw3a 903 Extend wff definition to include 3-way conjunction ('and').
 
Definitiondf-3or 904 Define disjunction ('or') of 3 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 660.
 
Definitiondf-3an 905 Define conjunction ('and') of 3 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 381.
 
Theorem3orass 906 Associative law for triple disjunction.
 
Theorem3anass 907 Associative law for triple conjunction.
 
Theorem3anrot 908 Rotation law for triple conjunction.
 
Theorem3orrot 909 Rotation law for triple disjunction.
 
Theorem3ancoma 910 Commutation law for triple conjunction.
 
Theorem3ancomb 911 Commutation law for triple conjunction.
 
Theorem3orcomb 912 Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.)
 
Theorem3anrev 913 Reversal law for triple conjunction.
 
Theorem3anor 914 Triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.)
 
Theorem3ianor 915 Negated triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.) (The proof was shortened by Andrew Salmon, 13-May-2011.)
 
Theorem3ioran 916 Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)
 
Theorem3oran 917 Triple disjunction in terms of triple conjunction.
 
Theorem3simpa 918 Simplification of triple conjunction.
 
Theorem3simpb 919 Simplification of triple conjunction.
 
Theorem3simpc 920 Simplification of triple conjunction. (The proof was shortened by Andrew Salmon, 13-May-2011.)
 
Theoremsimp1 921 Simplification of triple conjunction.
 
Theoremsimp2 922 Simplification of triple conjunction.
 
Theoremsimp3 923 Simplification of triple conjunction.
 
Theoremsimpl1 924 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
 
Theoremsimpl2 925 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
 
Theoremsimpl3 926 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
 
Theoremsimpr1 927 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
 
Theoremsimpr2 928 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
 
Theoremsimpr3 929 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
 
Theoremsimp1i 930 Infer a conjunct from a triple conjunction.
   =>   
 
Theoremsimp2i 931 Infer a conjunct from a triple conjunction.
   =>   
 
Theoremsimp3i 932 Infer a conjunct from a triple conjunction.
   =>   
 
Theoremsimp1d 933 Deduce a conjunct from a triple conjunction.
   =>   
 
Theoremsimp2d 934 Deduce a conjunct from a triple conjunction.
   =>   
 
Theoremsimp3d 935 Deduce a conjunct from a triple conjunction.
   =>   
 
Theoremsimp1bi 936 Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
   =>   
 
Theoremsimp2bi 937 Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
   =>   
 
Theoremsimp3bi 938 Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
   =>   
 
Theorem3adant1 939 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3adant2 940 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3adant3 941 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3ad2ant1 942 Deduction adding conjuncts to an antecedent.
   =>   
 
Theorem3ad2ant2 943 Deduction adding conjuncts to an antecedent.
   =>   
 
Theorem3ad2ant3 944 Deduction adding conjuncts to an antecedent.
   =>   
 
Theoremsimp1l 945 Simplification of triple conjunction.
 
Theoremsimp1r 946 Simplification of triple conjunction.
 
Theoremsimp2l 947 Simplification of triple conjunction.
 
Theoremsimp2r 948 Simplification of triple conjunction.
 
Theoremsimp3l 949 Simplification of triple conjunction.
 
Theoremsimp3r 950 Simplification of triple conjunction.
 
Theoremsimp11 951 Simplification of doubly triple conjunction.
 
Theoremsimp12 952 Simplification of doubly triple conjunction.
 
Theoremsimp13 953 Simplification of doubly triple conjunction.
 
Theoremsimp21 954 Simplification of doubly triple conjunction.
 
Theoremsimp22 955 Simplification of doubly triple conjunction.
 
Theoremsimp23 956 Simplification of doubly triple conjunction.
 
Theoremsimp31 957 Simplification of doubly triple conjunction.
 
Theoremsimp32 958 Simplification of doubly triple conjunction.
 
Theoremsimp33 959 Simplification of doubly triple conjunction.
 
Theoremsimpll1 960 Simplification of conjunction.
 
Theoremsimpll2 961 Simplification of conjunction.
 
Theoremsimpll3 962 Simplification of conjunction.
 
Theoremsimplr1 963 Simplification of conjunction.
 
Theoremsimplr2 964 Simplification of conjunction.
 
Theoremsimplr3 965 Simplification of conjunction.
 
Theoremsimprl1 966 Simplification of conjunction.
 
Theoremsimprl2 967 Simplification of conjunction.
 
Theoremsimprl3 968 Simplification of conjunction.
 
Theoremsimprr1 969 Simplification of conjunction.
 
Theoremsimprr2 970 Simplification of conjunction.
 
Theoremsimprr3 971 Simplification of conjunction.
 
Theoremsimpl1l 972 Simplification of conjunction.
 
Theoremsimpl1r 973 Simplification of conjunction.
 
Theoremsimpl2l 974 Simplification of conjunction.
 
Theoremsimpl2r 975 Simplification of conjunction.
 
Theoremsimpl3l 976 Simplification of conjunction.
 
Theoremsimpl3r 977 Simplification of conjunction.
 
Theoremsimpr1l 978 Simplification of conjunction.
 
Theoremsimpr1r 979 Simplification of conjunction.
 
Theoremsimpr2l 980 Simplification of conjunction.
 
Theoremsimpr2r 981 Simplification of conjunction.
 
Theoremsimpr3l 982 Simplification of conjunction.
 
Theoremsimpr3r 983 Simplification of conjunction.
 
Theoremsimp1ll 984 Simplification of conjunction.
 
Theoremsimp1lr 985 Simplification of conjunction.
 
Theoremsimp1rl 986 Simplification of conjunction.
 
Theoremsimp1rr 987 Simplification of conjunction.
 
Theoremsimp2ll 988 Simplification of conjunction.
 
Theoremsimp2lr 989 Simplification of conjunction.
 
Theoremsimp2rl 990 Simplification of conjunction.
 
Theoremsimp2rr 991 Simplification of conjunction.
 
Theoremsimp3ll 992 Simplification of conjunction.
 
Theoremsimp3lr 993 Simplification of conjunction.
 
Theoremsimp3rl 994 Simplification of conjunction.
 
Theoremsimp3rr 995 Simplification of conjunction.
 
Theoremsimpl11 996 Simplification of conjunction.
 
Theoremsimpl12 997 Simplification of conjunction.
 
Theoremsimpl13 998 Simplification of conjunction.
 
Theoremsimpl21 999 Simplification of conjunction.
 
Theoremsimpl22 1000 Simplification of conjunction.
    < 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-1914
  Copyright terms: Public domain < Previous  Next >