Home | Metamath
Proof Explorer Theorem List (p. 13 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | simp213 1201 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp221 1202 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp222 1203 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp223 1204 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp231 1205 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp232 1206 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp233 1207 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp311 1208 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp312 1209 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp313 1210 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp321 1211 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp322 1212 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp323 1213 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp331 1214 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp332 1215 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | simp333 1216 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Theorem | 3adantl1 1217 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
Theorem | 3adantl2 1218 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
Theorem | 3adantl3 1219 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
Theorem | 3adantr1 1220 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
Theorem | 3adantr2 1221 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
Theorem | 3adantr3 1222 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
Theorem | 3ad2antl1 1223 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
Theorem | 3ad2antl2 1224 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
Theorem | 3ad2antl3 1225 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
Theorem | 3ad2antr1 1226 | Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.) |
Theorem | 3ad2antr2 1227 | Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.) |
Theorem | 3ad2antr3 1228 | Deduction adding conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.) |
Theorem | 3anibar 1229 | Remove a hypothesis from the second member of a biimplication. (Contributed by FL, 22-Jul-2008.) |
Theorem | 3mix1 1230 | Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.) |
Theorem | 3mix2 1231 | Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.) |
Theorem | 3mix3 1232 | Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.) |
Theorem | 3mix1i 1233 | Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.) |
Theorem | 3mix2i 1234 | Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.) |
Theorem | 3mix3i 1235 | Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.) |
Theorem | 3mix1d 1236 | Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.) |
Theorem | 3mix2d 1237 | Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.) |
Theorem | 3mix3d 1238 | Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.) |
Theorem | 3pm3.2i 1239 | Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.) |
Theorem | pm3.2an3 1240 | Version of pm3.2 463 for a triple conjunction. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by Kyle Wyonch, 24-Apr-2021.) |
Theorem | pm3.2an3OLD 1241 | Obsolete proof of pm3.2an3 1240 as of 24-Apr-2021. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | 3jca 1242 | Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.) |
Theorem | 3jcad 1243 | Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.) |
Theorem | mpbir3an 1244 | Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.) |
Theorem | mpbir3and 1245 | Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.) (Revised by Mario Carneiro, 9-Jan-2015.) |
Theorem | syl3anbrc 1246 | Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.) |
Theorem | 3anim123i 1247 | Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.) |
Theorem | 3anim1i 1248 | Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.) |
Theorem | 3anim2i 1249 | Add two conjuncts to antecedent and consequent. (Contributed by AV, 21-Nov-2019.) |
Theorem | 3anim3i 1250 | Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.) |
Theorem | 3anbi123i 1251 | Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.) |
Theorem | 3orbi123i 1252 | Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.) |
Theorem | 3anbi1i 1253 | Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
Theorem | 3anbi2i 1254 | Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
Theorem | 3anbi3i 1255 | Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
Theorem | 3imp 1256 | Importation inference. (Contributed by NM, 8-Apr-1994.) |
Theorem | 3imp31 1257 | The importation inference 3imp 1256 with commutation of the first and third conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.) |
Theorem | 3imp231 1258 | Importation inference. (Contributed by Alan Sare, 17-Oct-2017.) |
Theorem | 3impa 1259 | Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
Theorem | 3impb 1260 | Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
Theorem | 3impia 1261 | Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) |
Theorem | 3impib 1262 | Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) |
Theorem | ex3 1263 | Apply ex 450 to a hypothesis with a 3-right-nested conjunction antecedent, with the antecedent of the assertion being a triple conjunction rather than a 2-right-nested conjunction. (Contributed by Alan Sare, 22-Apr-2018.) |
Theorem | 3exp 1264 | Exportation inference. (Contributed by NM, 30-May-1994.) |
Theorem | 3expa 1265 | Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
Theorem | 3expb 1266 | Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
Theorem | 3expia 1267 | Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) |
Theorem | 3expib 1268 | Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) |
Theorem | 3com12 1269 | Commutation in antecedent. Swap 1st and 2nd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | 3com13 1270 | Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) |
Theorem | 3com23 1271 | Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.) |
Theorem | 3coml 1272 | Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.) |
Theorem | 3comr 1273 | Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.) |
Theorem | 3adant3r1 1274 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.) |
Theorem | 3adant3r2 1275 | Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.) |
Theorem | 3adant3r3 1276 | Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.) |
Theorem | 3imp21 1277 | The importation inference 3imp 1256 with commutation of the first and second conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.) |
Theorem | 3imp3i2an 1278 | An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) |
Theorem | 3an1rs 1279 | Swap conjuncts. (Contributed by NM, 16-Dec-2007.) |
Theorem | 3imp1 1280 | Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.) |
Theorem | 3impd 1281 | Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.) |
Theorem | 3imp2 1282 | Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.) |
Theorem | 3exp1 1283 | Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.) |
Theorem | 3expd 1284 | Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.) |
Theorem | 3exp2 1285 | Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.) |
Theorem | exp5o 1286 | A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
Theorem | exp516 1287 | A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
Theorem | exp520 1288 | A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
Theorem | 3impexp 1289 | Version of impexp 462 for a triple conjunction. (Contributed by Alan Sare, 31-Dec-2011.) |
Theorem | 3anassrs 1290 | Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | 3an4anass 1291 | Associative law for four conjunctions with a triple conjunction. (Contributed by Alexander van der Vekens, 24-Jun-2018.) |
Theorem | ad4ant13 1292 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
Theorem | ad4ant14 1293 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
Theorem | ad4ant123 1294 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
Theorem | ad4ant124 1295 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
Theorem | ad4ant134 1296 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
Theorem | ad4ant23 1297 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
Theorem | ad4ant24 1298 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
Theorem | ad4ant234 1299 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
Theorem | ad5ant12 1300 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |