Theorem List for Intuitionistic Logic Explorer - 901-1000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 3simpb 901 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
  
    |
|
Theorem | 3simpc 902 |
Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
(Proof shortened by Andrew Salmon, 13-May-2011.)
|
  
    |
|
Theorem | simp1 903 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
  
  |
|
Theorem | simp2 904 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
  
  |
|
Theorem | simp3 905 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
  
  |
|
Theorem | simpl1 906 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
       |
|
Theorem | simpl2 907 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
       |
|
Theorem | simpl3 908 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
       |
|
Theorem | simpr1 909 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
    
  |
|
Theorem | simpr2 910 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
    
  |
|
Theorem | simpr3 911 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
    
  |
|
Theorem | simp1i 912 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
   |
|
Theorem | simp2i 913 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
   |
|
Theorem | simp3i 914 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
   |
|
Theorem | simp1d 915 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
       |
|
Theorem | simp2d 916 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
       |
|
Theorem | simp3d 917 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
       |
|
Theorem | simp1bi 918 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
       |
|
Theorem | simp2bi 919 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
       |
|
Theorem | simp3bi 920 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
       |
|
Theorem | 3adant1 921 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
         |
|
Theorem | 3adant2 922 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
      
  |
|
Theorem | 3adant3 923 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
      
  |
|
Theorem | 3ad2ant1 924 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
    
  |
|
Theorem | 3ad2ant2 925 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
       |
|
Theorem | 3ad2ant3 926 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
       |
|
Theorem | simp1l 927 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
   
   |
|
Theorem | simp1r 928 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
   
   |
|
Theorem | simp2l 929 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
       |
|
Theorem | simp2r 930 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
       |
|
Theorem | simp3l 931 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
    
  |
|
Theorem | simp3r 932 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
    
  |
|
Theorem | simp11 933 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
       |
|
Theorem | simp12 934 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
       |
|
Theorem | simp13 935 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
       |
|
Theorem | simp21 936 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
       |
|
Theorem | simp22 937 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
       |
|
Theorem | simp23 938 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
       |
|
Theorem | simp31 939 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
       |
|
Theorem | simp32 940 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
       |
|
Theorem | simp33 941 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
       |
|
Theorem | simpll1 942 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpll2 943 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpll3 944 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simplr1 945 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simplr2 946 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simplr3 947 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simprl1 948 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
    
    |
|
Theorem | simprl2 949 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
    
    |
|
Theorem | simprl3 950 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
    
    |
|
Theorem | simprr1 951 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simprr2 952 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simprr3 953 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpl1l 954 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpl1r 955 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpl2l 956 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpl2r 957 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpl3l 958 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
     
   |
|
Theorem | simpl3r 959 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
     
   |
|
Theorem | simpr1l 960 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
      
  |
|
Theorem | simpr1r 961 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
      
  |
|
Theorem | simpr2l 962 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
    
    |
|
Theorem | simpr2r 963 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
    
    |
|
Theorem | simpr3l 964 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
      
  |
|
Theorem | simpr3r 965 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
      
  |
|
Theorem | simp1ll 966 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simp1lr 967 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simp1rl 968 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
     
   |
|
Theorem | simp1rr 969 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
     
   |
|
Theorem | simp2ll 970 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simp2lr 971 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simp2rl 972 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simp2rr 973 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simp3ll 974 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simp3lr 975 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simp3rl 976 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simp3rr 977 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpl11 978 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpl12 979 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpl13 980 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpl21 981 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
    
    |
|
Theorem | simpl22 982 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
    
    |
|
Theorem | simpl23 983 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
    
    |
|
Theorem | simpl31 984 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpl32 985 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpl33 986 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpr11 987 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
    
    |
|
Theorem | simpr12 988 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
    
    |
|
Theorem | simpr13 989 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
    
    |
|
Theorem | simpr21 990 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpr22 991 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpr23 992 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpr31 993 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpr32 994 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simpr33 995 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simp1l1 996 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simp1l2 997 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simp1l3 998 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
         |
|
Theorem | simp1r1 999 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
      
  |
|
Theorem | simp1r2 1000 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
      
  |