Theorem List for Intuitionistic Logic Explorer - 1101-1200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 3impia 1101 |
Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|
           |
|
Theorem | 3impib 1102 |
Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|
       
   |
|
Theorem | 3exp 1103 |
Exportation inference. (Contributed by NM, 30-May-1994.)
|
      
    |
|
Theorem | 3expa 1104 |
Exportation from triple to double conjunction. (Contributed by NM,
20-Aug-1995.)
|
           |
|
Theorem | 3expb 1105 |
Exportation from triple to double conjunction. (Contributed by NM,
20-Aug-1995.)
|
     
     |
|
Theorem | 3expia 1106 |
Exportation from triple conjunction. (Contributed by NM,
19-May-2007.)
|
     
     |
|
Theorem | 3expib 1107 |
Exportation from triple conjunction. (Contributed by NM,
19-May-2007.)
|
           |
|
Theorem | 3com12 1108 |
Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM,
28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|
         |
|
Theorem | 3com13 1109 |
Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM,
28-Jan-1996.)
|
      
  |
|
Theorem | 3com23 1110 |
Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM,
28-Jan-1996.)
|
     

  |
|
Theorem | 3coml 1111 |
Commutation in antecedent. Rotate left. (Contributed by NM,
28-Jan-1996.)
|
      
  |
|
Theorem | 3comr 1112 |
Commutation in antecedent. Rotate right. (Contributed by NM,
28-Jan-1996.)
|
         |
|
Theorem | 3adant3r1 1113 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Feb-2008.)
|
     

 
  |
|
Theorem | 3adant3r2 1114 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
17-Feb-2008.)
|
     

 
  |
|
Theorem | 3adant3r3 1115 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
18-Feb-2008.)
|
     

 
  |
|
Theorem | 3an1rs 1116 |
Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
|
  
          |
|
Theorem | 3imp1 1117 |
Importation to left triple conjunction. (Contributed by NM,
24-Feb-2005.)
|
   
      
    |
|
Theorem | 3impd 1118 |
Importation deduction for triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
   
           |
|
Theorem | 3imp2 1119 |
Importation to right triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
   
           |
|
Theorem | 3exp1 1120 |
Exportation from left triple conjunction. (Contributed by NM,
24-Feb-2005.)
|
  
     
      |
|
Theorem | 3expd 1121 |
Exportation deduction for triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
         
     |
|
Theorem | 3exp2 1122 |
Exportation from right triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
    
   
      |
|
Theorem | exp5o 1123 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
    
    
         |
|
Theorem | exp516 1124 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
      
   
        |
|
Theorem | exp520 1125 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
  
   
   
        |
|
Theorem | 3anassrs 1126 |
Associative law for conjunction applied to antecedent (eliminates
syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)
|
    
          |
|
Theorem | 3adant1l 1127 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
        
  |
|
Theorem | 3adant1r 1128 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
           |
|
Theorem | 3adant2l 1129 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
     
     |
|
Theorem | 3adant2r 1130 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
     
     |
|
Theorem | 3adant3l 1131 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
     
  
  |
|
Theorem | 3adant3r 1132 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
     
  
  |
|
Theorem | syl12anc 1133 |
Syllogism combined with contraction. (Contributed by Jeff Hankins,
1-Aug-2009.)
|
               |
|
Theorem | syl21anc 1134 |
Syllogism combined with contraction. (Contributed by Jeff Hankins,
1-Aug-2009.)
|
               |
|
Theorem | syl3anc 1135 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
       
     |
|
Theorem | syl22anc 1136 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
              
    |
|
Theorem | syl13anc 1137 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                 |
|
Theorem | syl31anc 1138 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                 |
|
Theorem | syl112anc 1139 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
         
       |
|
Theorem | syl121anc 1140 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                 |
|
Theorem | syl211anc 1141 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                 |
|
Theorem | syl23anc 1142 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                     |
|
Theorem | syl32anc 1143 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                     |
|
Theorem | syl122anc 1144 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                     |
|
Theorem | syl212anc 1145 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                     |
|
Theorem | syl221anc 1146 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                     |
|
Theorem | syl113anc 1147 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
           

 
    |
|
Theorem | syl131anc 1148 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                   |
|
Theorem | syl311anc 1149 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
              
    |
|
Theorem | syl33anc 1150 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                
 
    |
|
Theorem | syl222anc 1151 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                         |
|
Theorem | syl123anc 1152 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                
 
    |
|
Theorem | syl132anc 1153 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
                       |
|
Theorem | syl213anc 1154 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                
 
    |
|
Theorem | syl231anc 1155 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                       |
|
Theorem | syl312anc 1156 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
                
 
    |
|
Theorem | syl321anc 1157 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
                       |
|
Theorem | syl133anc 1158 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                    
    |
|
Theorem | syl313anc 1159 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                  
      |
|
Theorem | syl331anc 1160 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                  
      |
|
Theorem | syl223anc 1161 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                           |
|
Theorem | syl232anc 1162 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                           |
|
Theorem | syl322anc 1163 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                           |
|
Theorem | syl233anc 1164 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                      
 
    |
|
Theorem | syl323anc 1165 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                      
 
    |
|
Theorem | syl332anc 1166 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
                    
   
    |
|
Theorem | syl333anc 1167 |
A syllogism inference combined with contraction. (Contributed by NM,
10-Mar-2012.)
|
                      
        |
|
Theorem | syl3an1 1168 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
       

  |
|
Theorem | syl3an2 1169 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
           |
|
Theorem | syl3an3 1170 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
        
  |
|
Theorem | syl3an1b 1171 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
   
       |
|
Theorem | syl3an2b 1172 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
   
       |
|
Theorem | syl3an3b 1173 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
   
       |
|
Theorem | syl3an1br 1174 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
   
       |
|
Theorem | syl3an2br 1175 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
   
       |
|
Theorem | syl3an3br 1176 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
   
       |
|
Theorem | syl3an 1177 |
A triple syllogism inference. (Contributed by NM, 13-May-2004.)
|
       
       |
|
Theorem | syl3anb 1178 |
A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
|
       
       |
|
Theorem | syl3anbr 1179 |
A triple syllogism inference. (Contributed by NM, 29-Dec-2011.)
|
       
       |
|
Theorem | syld3an3 1180 |
A syllogism inference. (Contributed by NM, 20-May-2007.)
|
     

  

  |
|
Theorem | syld3an1 1181 |
A syllogism inference. (Contributed by NM, 7-Jul-2008.)
|
     

      |
|
Theorem | syld3an2 1182 |
A syllogism inference. (Contributed by NM, 20-May-2007.)
|
     

  

  |
|
Theorem | syl3anl1 1183 |
A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|
          
    |
|
Theorem | syl3anl2 1184 |
A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|
               |
|
Theorem | syl3anl3 1185 |
A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|
               |
|
Theorem | syl3anl 1186 |
A triple syllogism inference. (Contributed by NM, 24-Dec-2006.)
|
         
    
    |
|
Theorem | syl3anr1 1187 |
A syllogism inference. (Contributed by NM, 31-Jul-2007.)
|
      
     
  |
|
Theorem | syl3anr2 1188 |
A syllogism inference. (Contributed by NM, 1-Aug-2007.)
|
      
   
 
  |
|
Theorem | syl3anr3 1189 |
A syllogism inference. (Contributed by NM, 23-Aug-2007.)
|
      
     
  |
|
Theorem | 3impdi 1190 |
Importation inference (undistribute conjunction). (Contributed by NM,
14-Aug-1995.)
|
             |
|
Theorem | 3impdir 1191 |
Importation inference (undistribute conjunction). (Contributed by NM,
20-Aug-1995.)
|
             |
|
Theorem | 3anidm12 1192 |
Inference from idempotent law for conjunction. (Contributed by NM,
7-Mar-2008.)
|
         |
|
Theorem | 3anidm13 1193 |
Inference from idempotent law for conjunction. (Contributed by NM,
7-Mar-2008.)
|
  
  
   |
|
Theorem | 3anidm23 1194 |
Inference from idempotent law for conjunction. (Contributed by NM,
1-Feb-2007.)
|
     
   |
|
Theorem | 3ori 1195 |
Infer implication from triple disjunction. (Contributed by NM,
26-Sep-2006.)
|
       |
|
Theorem | 3jao 1196 |
Disjunction of 3 antecedents. (Contributed by NM, 8-Apr-1994.)
|
               |
|
Theorem | 3jaob 1197 |
Disjunction of 3 antecedents. (Contributed by NM, 13-Sep-2011.)
|
               |
|
Theorem | 3jaoi 1198 |
Disjunction of 3 antecedents (inference). (Contributed by NM,
12-Sep-1995.)
|
           |
|
Theorem | 3jaod 1199 |
Disjunction of 3 antecedents (deduction). (Contributed by NM,
14-Oct-2005.)
|
         
         |
|
Theorem | 3jaoian 1200 |
Disjunction of 3 antecedents (inference). (Contributed by NM,
14-Oct-2005.)
|
                   |