| Metamath Proof Explorer | < Previous Next > | |
| Browser slow? Try the
Unicode version. |
| Color key: | (1-11415) |
(11416-13002) |
(13003-19465) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | syl313anc 1401 | Syllogism combined with contraction. |
| Theorem | syl331anc 1402 | Syllogism combined with contraction. |
| Theorem | syl223anc 1403 | Syllogism combined with contraction. |
| Theorem | syl232anc 1404 | Syllogism combined with contraction. |
| Theorem | syl322anc 1405 | Syllogism combined with contraction. |
| Theorem | syl233anc 1406 | Syllogism combined with contraction. |
| Theorem | syl323anc 1407 | Syllogism combined with contraction. |
| Theorem | syl332anc 1408 | Syllogism combined with contraction. |
| Theorem | syl333anc 1409 | A syllogism inference combined with contraction. |
| Theorem | syl3an1 1410 | A syllogism inference. |
| Theorem | syl3an2 1411 | A syllogism inference. |
| Theorem | syl3an3 1412 | A syllogism inference. |
| Theorem | syl3an1b 1413 | A syllogism inference. |
| Theorem | syl3an2b 1414 | A syllogism inference. |
| Theorem | syl3an3b 1415 | A syllogism inference. |
| Theorem | syl3an1br 1416 | A syllogism inference. |
| Theorem | syl3an2br 1417 | A syllogism inference. |
| Theorem | syl3an3br 1418 | A syllogism inference. |
| Theorem | syl3an 1419 | A triple syllogism inference. |
| Theorem | syl3anb 1420 | A triple syllogism inference. |
| Theorem | syl3anbr 1421 | A triple syllogism inference. |
| Theorem | syld3an3 1422 | A syllogism inference. |
| Theorem | syld3an1 1423 | A syllogism inference. |
| Theorem | syld3an2 1424 | A syllogism inference. |
| Theorem | syl3an1OLD 1425 | A syllogism inference. |
| Theorem | syl3an2OLD 1426 | A syllogism inference. |
| Theorem | syl3an3OLD 1427 | A syllogism inference. |
| Theorem | syl3an1bOLD 1428 | A syllogism inference. |
| Theorem | syl3an2bOLD 1429 | A syllogism inference. |
| Theorem | syl3an3bOLD 1430 | A syllogism inference. |
| Theorem | syl3an1brOLD 1431 | A syllogism inference. |
| Theorem | syl3an2brOLD 1432 | A syllogism inference. |
| Theorem | syl3an3brOLD 1433 | A syllogism inference. |
| Theorem | syl3anOLD 1434 | A triple syllogism inference. |
| Theorem | syl3anbOLD 1435 | A triple syllogism inference. |
| Theorem | syl3anbrOLD 1436 | A triple syllogism inference. |
| Theorem | syld3an3OLD 1437 | A syllogism inference. |
| Theorem | syld3an1OLD 1438 | A syllogism inference. |
| Theorem | syld3an2OLD 1439 | A syllogism inference. |
| Theorem | syl3anl1 1440 | A syllogism inference. |
| Theorem | syl3anl2 1441 | A syllogism inference. |
| Theorem | syl3anl3 1442 | A syllogism inference. |
| Theorem | syl3anl 1443 | A triple syllogism inference. |
| Theorem | syl3anl1OLD 1444 | A syllogism inference. |
| Theorem | syl3anl2OLD 1445 | A syllogism inference. |
| Theorem | syl3anl3OLD 1446 | A syllogism inference. |
| Theorem | syl3anlOLD 1447 | A triple syllogism inference. |
| Theorem | syl3anr1 1448 | A syllogism inference. |
| Theorem | syl3anr2 1449 | A syllogism inference. |
| Theorem | syl3anr3 1450 | A syllogism inference. |
| Theorem | syl3anr1OLD 1451 | A syllogism inference. |
| Theorem | syl3anr2OLD 1452 | A syllogism inference. |
| Theorem | syl3anr3OLD 1453 | A syllogism inference. |
| Theorem | 3impdi 1454 | Importation inference (undistribute conjunction). |
| Theorem | 3impdir 1455 | Importation inference (undistribute conjunction). |
| Theorem | 3anidm12 1456 | Inference from idempotent law for conjunction. |
| Theorem | 3anidm13 1457 | Inference from idempotent law for conjunction. |
| Theorem | 3anidm23 1458 | Inference from idempotent law for conjunction. |
| Theorem | 3ori 1459 | Infer implication from triple disjunction. |
| Theorem | 3jao 1460 | Disjunction of 3 antecedents. |
| Theorem | 3jaob 1461 | Disjunction of 3 antecedents. |
| Theorem | 3jaoi 1462 | Disjunction of 3 antecedents (inference). |
| Theorem | 3jaod 1463 | Disjunction of 3 antecedents (deduction). |
| Theorem | 3jaoian 1464 | Disjunction of 3 antecedents (inference). |
| Theorem | 3jaodan 1465 | Disjunction of 3 antecedents (deduction). |
| Theorem | 3jaao 1466 | Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009.) (The proof was shortened by Andrew Salmon, 13-May-2011.) |
| Theorem | syl3an9b 1467 | Nested syllogism inference conjoining 3 dissimilar antecedents. |
| Theorem | 3orbi123d 1468 | Deduction joining 3 equivalences to form equivalence of disjunctions. |
| Theorem | 3anbi123d 1469 | Deduction joining 3 equivalences to form equivalence of conjunctions. |
| Theorem | 3anbi12d 1470 | Deduction conjoining and adding a conjunct to equivalences. |
| Theorem | 3anbi13d 1471 | Deduction conjoining and adding a conjunct to equivalences. |
| Theorem | 3anbi23d 1472 | Deduction conjoining and adding a conjunct to equivalences. |
| Theorem | 3anbi1d 1473 | Deduction adding conjuncts to an equivalence. |
| Theorem | 3anbi2d 1474 | Deduction adding conjuncts to an equivalence. |
| Theorem | 3anbi3d 1475 | Deduction adding conjuncts to an equivalence. |
| Theorem | 3anim123d 1476 | Deduction joining 3 implications to form implication of conjunctions. |
| Theorem | 3orim123d 1477 | Deduction joining 3 implications to form implication of disjunctions. |
| Theorem | an6 1478 | Rearrangement of 6 conjuncts. |
| Theorem | 3an6 1479 | Analogue of an4 939 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Theorem | 3or6 1480 | Analogue of or4 586 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) |
| Theorem | mp3an1 1481 | An inference based on modus ponens. |
| Theorem | mp3an2 1482 | An inference based on modus ponens. |
| Theorem | mp3an3 1483 | An inference based on modus ponens. |
| Theorem | mp3an12 1484 | An inference based on modus ponens. |
| Theorem | mp3an13 1485 | An inference based on modus ponens. |
| Theorem | mp3an23 1486 | An inference based on modus ponens. |
| Theorem | mp3an1i 1487 | An inference based on modus ponens. |
| Theorem | mp3anl1 1488 | An inference based on modus ponens. |
| Theorem | mp3anl2 1489 | An inference based on modus ponens. |
| Theorem | mp3anl3 1490 | An inference based on modus ponens. |
| Theorem | mp3anr1 1491 | An inference based on modus ponens. |
| Theorem | mp3anr2 1492 | An inference based on modus ponens. |
| Theorem | mp3anr3 1493 | An inference based on modus ponens. |
| Theorem | mp3an 1494 | An inference based on modus ponens. |
| Theorem | mpd3an3 1495 | An inference based on modus ponens. |
| Theorem | mpd3an23 1496 | An inference based on modus ponens. |
| Theorem | biimp3a 1497 | Infer implication from a logical equivalence. Similar to biimpa 711. |
| Theorem | biimp3ar 1498 | Infer implication from a logical equivalence. Similar to biimpar 712. |
| Theorem | 3anandis 1499 | Inference that undistributes a triple conjunction in the antecedent. |
| Theorem | 3anandirs 1500 | Inference that undistributes a triple conjunction in the antecedent. |
| MPE Home Contents | Copyright terms: Public domain | < Previous Next > |