HomeHome Intuitionistic Logic Explorer
Theorem List (p. 12 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 - 1101-1200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremsyl3anbrc 1101 Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
   &       &       &       =>   
 
Theorem3anim123i 1102 Join antecedents and consequents with conjunction.
   &       &       =>   
 
Theorem3anim1i 1103 Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)
   =>   
 
Theorem3anim3i 1104 Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)
   =>   
 
Theorem3anbi123i 1105 Join 3 biconditionals with conjunction.
   &       &       =>   
 
Theorem3orbi123i 1106 Join 3 biconditionals with disjunction.
   &       &       =>   
 
Theorem3anbi1i 1107 Inference adding two conjuncts to each side of a biconditional.
   =>   
 
Theorem3anbi2i 1108 Inference adding two conjuncts to each side of a biconditional.
   =>   
 
Theorem3anbi3i 1109 Inference adding two conjuncts to each side of a biconditional.
   =>   
 
Theorem3imp 1110 Importation inference.
   =>   
 
Theorem3impa 1111 Importation from double to triple conjunction.
   =>   
 
Theorem3impb 1112 Importation from double to triple conjunction.
   =>   
 
Theorem3impia 1113 Importation to triple conjunction.
   =>   
 
Theorem3impib 1114 Importation to triple conjunction.
   =>   
 
Theorem3exp 1115 Exportation inference.
   =>   
 
Theorem3expa 1116 Exportation from triple to double conjunction.
   =>   
 
Theorem3expb 1117 Exportation from triple to double conjunction.
   =>   
 
Theorem3expia 1118 Exportation from triple conjunction.
   =>   
 
Theorem3expib 1119 Exportation from triple conjunction.
   =>   
 
Theorem3com12 1120 Commutation in antecedent. Swap 1st and 3rd. (The proof was shortened by Andrew Salmon, 13-May-2011.)
   =>   
 
Theorem3com13 1121 Commutation in antecedent. Swap 1st and 3rd.
   =>   
 
Theorem3com23 1122 Commutation in antecedent. Swap 2nd and 3rd.
   =>   
 
Theorem3coml 1123 Commutation in antecedent. Rotate left.
   =>   
 
Theorem3comr 1124 Commutation in antecedent. Rotate right.
   =>   
 
Theorem3adant3r1 1125 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3adant3r2 1126 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3adant3r3 1127 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3an1rs 1128 Swap conjuncts.
   =>   
 
Theorem3imp1 1129 Importation to left triple conjunction.
   =>   
 
Theorem3impd 1130 Importation deduction for triple conjunction.
   =>   
 
Theorem3imp2 1131 Importation to right triple conjunction.
   =>   
 
Theorem3exp1 1132 Exportation from left triple conjunction.
   =>   
 
Theorem3expd 1133 Exportation deduction for triple conjunction.
   =>   
 
Theorem3exp2 1134 Exportation from right triple conjunction.
   =>   
 
Theoremexp5o 1135 A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
   =>   
 
Theoremexp516 1136 A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
   =>   
 
Theoremexp520 1137 A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
   =>   
 
Theorem3adant1l 1138 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3adant1r 1139 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3adant2l 1140 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3adant2r 1141 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3adant3l 1142 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3adant3r 1143 Deduction adding a conjunct to antecedent.
   =>   
 
Theoremsyl12anc 1144 Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
   &       &       &       =>   
 
Theoremsyl21anc 1145 Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
   &       &       &       =>   
 
Theoremsyl3anc 1146 Syllogism combined with contraction.
   &       &       &       =>   
 
Theoremsyl22anc 1147 Syllogism combined with contraction.
   &       &       &       &       =>   
 
Theoremsyl13anc 1148 Syllogism combined with contraction.
   &       &       &       &       =>   
 
Theoremsyl31anc 1149 Syllogism combined with contraction.
   &       &       &       &       =>   
 
Theoremsyl112anc 1150 Syllogism combined with contraction.
   &       &       &       &       =>   
 
Theoremsyl121anc 1151 Syllogism combined with contraction.
   &       &       &       &       =>   
 
Theoremsyl211anc 1152 Syllogism combined with contraction.
   &       &       &       &       =>   
 
Theoremsyl23anc 1153 Syllogism combined with contraction.
   &       &       &       &       &       =>   
 
Theoremsyl32anc 1154 Syllogism combined with contraction.
   &       &       &       &       &       =>   
 
Theoremsyl122anc 1155 Syllogism combined with contraction.
   &       &       &       &       &       =>   
 
Theoremsyl212anc 1156 Syllogism combined with contraction.
   &       &       &       &       &       =>   
 
Theoremsyl221anc 1157 Syllogism combined with contraction.
   &       &       &       &       &       =>   
 
Theoremsyl113anc 1158 Syllogism combined with contraction.
   &       &       &       &       &       =>   
 
Theoremsyl131anc 1159 Syllogism combined with contraction.
   &       &       &       &       &       =>   
 
Theoremsyl311anc 1160 Syllogism combined with contraction.
   &       &       &       &       &       =>   
 
Theoremsyl33anc 1161 Syllogism combined with contraction.
   &       &       &       &       &       &       =>   
 
Theoremsyl222anc 1162 Syllogism combined with contraction.
   &       &       &       &       &       &       =>   
 
Theoremsyl123anc 1163 Syllogism combined with contraction.
   &       &       &       &       &       &       =>   
 
Theoremsyl132anc 1164 Syllogism combined with contraction.
   &       &       &       &       &       &       =>   
 
Theoremsyl213anc 1165 Syllogism combined with contraction.
   &       &       &       &       &       &       =>   
 
Theoremsyl231anc 1166 Syllogism combined with contraction.
   &       &       &       &       &       &       =>   
 
Theoremsyl312anc 1167 Syllogism combined with contraction.
   &       &       &       &       &       &       =>   
 
Theoremsyl321anc 1168 Syllogism combined with contraction.
   &       &       &       &       &       &       =>   
 
Theoremsyl133anc 1169 Syllogism combined with contraction.
   &       &       &       &       &       &       &       =>   
 
Theoremsyl313anc 1170 Syllogism combined with contraction.
   &       &       &       &       &       &       &       =>   
 
Theoremsyl331anc 1171 Syllogism combined with contraction.
   &       &       &       &       &       &       &       =>   
 
Theoremsyl223anc 1172 Syllogism combined with contraction.
   &       &       &       &       &       &       &       =>   
 
Theoremsyl232anc 1173 Syllogism combined with contraction.
   &       &       &       &       &       &       &       =>   
 
Theoremsyl322anc 1174 Syllogism combined with contraction.
   &       &       &       &       &       &       &       =>   
 
Theoremsyl233anc 1175 Syllogism combined with contraction.
   &       &       &       &       &       &       &       &       =>   
 
Theoremsyl323anc 1176 Syllogism combined with contraction.
   &       &       &       &       &       &       &       &       =>   
 
Theoremsyl332anc 1177 Syllogism combined with contraction.
   &       &       &       &       &       &       &       &       =>   
 
Theoremsyl333anc 1178 A syllogism inference combined with contraction.
   &       &       &       &       &       &       &       &       &       =>   
 
Theoremsyl3an1 1179 A syllogism inference.
   &       =>   
 
Theoremsyl3an2 1180 A syllogism inference.
   &       =>   
 
Theoremsyl3an3 1181 A syllogism inference.
   &       =>   
 
Theoremsyl3an1b 1182 A syllogism inference.
   &       =>   
 
Theoremsyl3an2b 1183 A syllogism inference.
   &       =>   
 
Theoremsyl3an3b 1184 A syllogism inference.
   &       =>   
 
Theoremsyl3an1br 1185 A syllogism inference.
   &       =>   
 
Theoremsyl3an2br 1186 A syllogism inference.
   &       =>   
 
Theoremsyl3an3br 1187 A syllogism inference.
   &       =>   
 
Theoremsyl3an 1188 A triple syllogism inference.
   &       &       &       =>   
 
Theoremsyl3anb 1189 A triple syllogism inference.
   &       &       &       =>   
 
Theoremsyl3anbr 1190 A triple syllogism inference.
   &       &       &       =>   
 
Theoremsyld3an3 1191 A syllogism inference.
   &       =>   
 
Theoremsyld3an1 1192 A syllogism inference.
   &       =>   
 
Theoremsyld3an2 1193 A syllogism inference.
   &       =>   
 
Theoremsyl3anl1 1194 A syllogism inference.
   &       =>   
 
Theoremsyl3anl2 1195 A syllogism inference.
   &       =>   
 
Theoremsyl3anl3 1196 A syllogism inference.
   &       =>   
 
Theoremsyl3anl 1197 A triple syllogism inference.
   &       &       &       =>   
 
Theoremsyl3anr1 1198 A syllogism inference.
   &       =>   
 
Theoremsyl3anr2 1199 A syllogism inference.
   &       =>   
 
Theoremsyl3anr3 1200 A syllogism inference.
   &       =>   
    < 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 >