HomeHome Intuitionistic Logic Explorer
Theorem List (p. 12 of 22)
< 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
 
Theoremsyl132anc 1101 Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
   &       &       &       &       &       &       =>   
 
Theoremsyl213anc 1102 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       &       =>   
 
Theoremsyl231anc 1103 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       &       =>   
 
Theoremsyl312anc 1104 Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
   &       &       &       &       &       &       =>   
 
Theoremsyl321anc 1105 Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
   &       &       &       &       &       &       =>   
 
Theoremsyl133anc 1106 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       &       &       =>   
 
Theoremsyl313anc 1107 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       &       &       =>   
 
Theoremsyl331anc 1108 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       &       &       =>   
 
Theoremsyl223anc 1109 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       &       &       =>   
 
Theoremsyl232anc 1110 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       &       &       =>   
 
Theoremsyl322anc 1111 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       &       &       =>   
 
Theoremsyl233anc 1112 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       &       &       &       =>   
 
Theoremsyl323anc 1113 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       &       &       &       =>   
 
Theoremsyl332anc 1114 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       &       &       &       =>   
 
Theoremsyl333anc 1115 A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012.)
   &       &       &       &       &       &       &       &       &       =>   
 
Theoremsyl3an1 1116 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
   &       =>   
 
Theoremsyl3an2 1117 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
   &       =>   
 
Theoremsyl3an3 1118 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
   &       =>   
 
Theoremsyl3an1b 1119 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
   &       =>   
 
Theoremsyl3an2b 1120 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
   &       =>   
 
Theoremsyl3an3b 1121 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
   &       =>   
 
Theoremsyl3an1br 1122 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
   &       =>   
 
Theoremsyl3an2br 1123 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
   &       =>   
 
Theoremsyl3an3br 1124 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
   &       =>   
 
Theoremsyl3an 1125 A triple syllogism inference. (Contributed by NM, 13-May-2004.)
   &       &       &       =>   
 
Theoremsyl3anb 1126 A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
   &       &       &       =>   
 
Theoremsyl3anbr 1127 A triple syllogism inference. (Contributed by NM, 29-Dec-2011.)
   &       &       &       =>   
 
Theoremsyld3an3 1128 A syllogism inference. (Contributed by NM, 20-May-2007.)
   &       =>   
 
Theoremsyld3an1 1129 A syllogism inference. (Contributed by NM, 7-Jul-2008.)
   &       =>   
 
Theoremsyld3an2 1130 A syllogism inference. (Contributed by NM, 20-May-2007.)
   &       =>   
 
Theoremsyl3anl1 1131 A syllogism inference. (Contributed by NM, 24-Feb-2005.)
   &       =>   
 
Theoremsyl3anl2 1132 A syllogism inference. (Contributed by NM, 24-Feb-2005.)
   &       =>   
 
Theoremsyl3anl3 1133 A syllogism inference. (Contributed by NM, 24-Feb-2005.)
   &       =>   
 
Theoremsyl3anl 1134 A triple syllogism inference. (Contributed by NM, 24-Dec-2006.)
   &       &       &       =>   
 
Theoremsyl3anr1 1135 A syllogism inference. (Contributed by NM, 31-Jul-2007.)
   &       =>   
 
Theoremsyl3anr2 1136 A syllogism inference. (Contributed by NM, 1-Aug-2007.)
   &       =>   
 
Theoremsyl3anr3 1137 A syllogism inference. (Contributed by NM, 23-Aug-2007.)
   &       =>   
 
Theorem3impdi 1138 Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.)
   =>   
 
Theorem3impdir 1139 Importation inference (undistribute conjunction). (Contributed by NM, 20-Aug-1995.)
   =>   
 
Theorem3anidm12 1140 Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
   =>   
 
Theorem3anidm13 1141 Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
   =>   
 
Theorem3anidm23 1142 Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)
   =>   
 
Theorem3ori 1143 Infer implication from triple disjunction. (Contributed by NM, 26-Sep-2006.)
   =>   
 
Theorem3jao 1144 Disjunction of 3 antecedents. (Contributed by NM, 8-Apr-1994.)
 
Theorem3jaob 1145 Disjunction of 3 antecedents. (Contributed by NM, 13-Sep-2011.)
 
Theorem3jaoi 1146 Disjunction of 3 antecedents (inference). (Contributed by NM, 12-Sep-1995.)
   &       &       =>   
 
Theorem3jaod 1147 Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
   &       &       =>   
 
Theorem3jaoian 1148 Disjunction of 3 antecedents (inference). (Contributed by NM, 14-Oct-2005.)
   &       &       =>   
 
Theorem3jaodan 1149 Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
   &       &       =>   
 
Theorem3jaao 1150 Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.)
   &       &       =>   
 
Theoremsyl3an9b 1151 Nested syllogism inference conjoining 3 dissimilar antecedents. (Contributed by NM, 1-May-1995.)
   &       &       =>   
 
Theorem3orbi123d 1152 Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994.)
   &       &       =>   
 
Theorem3anbi123d 1153 Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)
   &       &       =>   
 
Theorem3anbi12d 1154 Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
   &       =>   
 
Theorem3anbi13d 1155 Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
   &       =>   
 
Theorem3anbi23d 1156 Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
   &       =>   
 
Theorem3anbi1d 1157 Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
   =>   
 
Theorem3anbi2d 1158 Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
   =>   
 
Theorem3anbi3d 1159 Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
   =>   
 
Theorem3anim123d 1160 Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.)
   &       &       =>   
 
Theorem3orim123d 1161 Deduction joining 3 implications to form implication of disjunctions. (Contributed by NM, 4-Apr-1997.)
   &       &       =>   
 
Theoreman6 1162 Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995.)
 
Theorem3an6 1163 Analog of an4 502 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 
Theorem3or6 1164 Analog of or4 666 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.)
 
Theoremmp3an1 1165 An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
   &       =>   
 
Theoremmp3an2 1166 An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
   &       =>   
 
Theoremmp3an3 1167 An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
   &       =>   
 
Theoremmp3an12 1168 An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
   &       &       =>   
 
Theoremmp3an13 1169 An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
   &       &       =>   
 
Theoremmp3an23 1170 An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
   &       &       =>   
 
Theoremmp3an1i 1171 An inference based on modus ponens. (Contributed by NM, 5-Jul-2005.)
   &       =>   
 
Theoremmp3anl1 1172 An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
   &       =>   
 
Theoremmp3anl2 1173 An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
   &       =>   
 
Theoremmp3anl3 1174 An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
   &       =>   
 
Theoremmp3anr1 1175 An inference based on modus ponens. (Contributed by NM, 4-Nov-2006.)
   &       =>   
 
Theoremmp3anr2 1176 An inference based on modus ponens. (Contributed by NM, 24-Nov-2006.)
   &       =>   
 
Theoremmp3anr3 1177 An inference based on modus ponens. (Contributed by NM, 19-Oct-2007.)
   &       =>   
 
Theoremmp3an 1178 An inference based on modus ponens. (Contributed by NM, 14-May-1999.)
   &       &       &       =>   
 
Theoremmpd3an3 1179 An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)
   &       =>   
 
Theoremmpd3an23 1180 An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.)
   &       &       =>   
 
Theorembiimp3a 1181 Infer implication from a logical equivalence. Similar to biimpa 278. (Contributed by NM, 4-Sep-2005.)
   =>   
 
Theorembiimp3ar 1182 Infer implication from a logical equivalence. Similar to biimpar 279. (Contributed by NM, 2-Jan-2009.)
   =>   
 
Theorem3anandis 1183 Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 18-Apr-2007.)
   =>   
 
Theorem3anandirs 1184 Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 25-Jul-2006.) (Revised by NM, 18-Apr-2007.)
   =>   
 
Theoremecased 1185 Elimination by cases based on a disjunction (rather than an implication) does hold intuitionistically. However, it is more of a curiosity than something useful in proofs, because in intuitionistic logic it will be just as hard to prove as it would be to prove one of or . (Contributed by Jim Kingdon, 9-Dec-2017.)
   &       =>   
 
Theoremecase23d 1186 Variation of ecased 1185 with three disjuncts instead of two. (Contributed by NM, 22-Apr-1994.) (Revised by Jim Kingdon, 9-Dec-2017.)
   &       &       =>   
 
1.2.11  True and false constants
 
Syntaxwtru 1187 is a wff.
 
Syntaxwfal 1188 is a wff.
 
Theoremtrujust 1189 Soundness justification theorem for df-tru 1190. (Contributed by NM, 17-Nov-2013.)
 
Definitiondf-tru 1190 Definition of , a tautology. is a constant true. In this definition biid 158 is used as an antecedent, however, any true wff, such as an axiom, can be used in its place. (Contributed by Anthony Hart, 13-Oct-2010.)
 
Definitiondf-fal 1191 Definition of , a contradiction. is a constant false. (Contributed by Anthony Hart, 13-Oct-2010.)
 
Theoremtru 1192 is provable. (Contributed by Anthony Hart, 13-Oct-2010.)
 
Theoremfal 1193 is not provable. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Mel L. O'Cat, 11-Mar-2012.)
 
Theoremtrud 1194 Eliminate as an antecedent. (Contributed by Mario Carneiro, 13-Mar-2014.)
   =>   
 
Theoremtbtru 1195 If something is true, it outputs . (Contributed by Anthony Hart, 14-Aug-2011.)
 
Theoremnbfal 1196 If something is not true, it outputs . (Contributed by Anthony Hart, 14-Aug-2011.)
 
Theorembitru 1197 A theorem is equivalent to truth. (Contributed by Mario Carneiro, 9-May-2015.)
   =>   
 
Theorembifal 1198 A contradiction is equivalent to falsehood. (Contributed by Mario Carneiro, 9-May-2015.)
   =>   
 
Theoremfalim 1199 implies anything. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.)
 
Theoremfalimd 1200 implies anything. (Contributed by Mario Carneiro, 9-Feb-2017.)
    < 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-2186
  Copyright terms: Public domain < Previous  Next >