Home | Metamath
Proof Explorer Theorem List (p. 5 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 | pm1.4 401 | Axiom *1.4 of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) |
Theorem | orcom 402 | Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 15-Nov-2012.) |
Theorem | orcomd 403 | Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.) |
Theorem | orcoms 404 | Commutation of disjuncts in antecedent. (Contributed by NM, 2-Dec-2012.) |
Theorem | orci 405 | Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.) |
Theorem | olci 406 | Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.) |
Theorem | orcd 407 | Deduction introducing a disjunct. A translation of natural deduction rule IR ( insertion right), see natded 27260. (Contributed by NM, 20-Sep-2007.) |
Theorem | olcd 408 | Deduction introducing a disjunct. A translation of natural deduction rule IL ( insertion left), see natded 27260. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
Theorem | orcs 409 | Deduction eliminating disjunct. Notational convention: We sometimes suffix with "s" the label of an inference that manipulates an antecedent, leaving the consequent unchanged. The "s" means that the inference eliminates the need for a syllogism (syl 17) -type inference in a proof. (Contributed by NM, 21-Jun-1994.) |
Theorem | olcs 410 | Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.) (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
Theorem | pm2.07 411 | Theorem *2.07 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.45 412 | Theorem *2.45 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.46 413 | Theorem *2.46 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.47 414 | Theorem *2.47 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.48 415 | Theorem *2.48 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.49 416 | Theorem *2.49 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.67-2 417 | Slight generalization of Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.67 418 | Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.25 419 | Theorem *2.25 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
Theorem | biorf 420 | A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of [WhiteheadRussell] p. 121. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2012.) |
Theorem | biortn 421 | A wff is equivalent to its negated disjunction with falsehood. (Contributed by NM, 9-Jul-2012.) |
Theorem | biorfi 422 | A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 16-Jul-2021.) |
Theorem | biorfiOLD 423 | Obsolete proof of biorfi 422 as of 16-Jul-2021. (Contributed by NM, 23-Mar-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | pm2.621 424 | Theorem *2.621 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.62 425 | Theorem *2.62 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Dec-2013.) |
Theorem | pm2.68 426 | Theorem *2.68 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
Theorem | dfor2 427 | Logical 'or' expressed in terms of implication only. Theorem *5.25 of [WhiteheadRussell] p. 124. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Wolf Lammen, 20-Oct-2012.) |
Theorem | imor 428 | Implication in terms of disjunction. Theorem *4.6 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) |
Theorem | imori 429 | Infer disjunction from implication. (Contributed by NM, 12-Mar-2012.) |
Theorem | imorri 430 | Infer implication from disjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | exmid 431 | Law of excluded middle, also called the principle of tertium non datur. Theorem *2.11 of [WhiteheadRussell] p. 101. It says that something is either true or not true; there are no in-between values of truth. This is an essential distinction of our classical logic and is not a theorem of intuitionistic logic. In intuitionistic logic, if this statement is true for some , then is decideable. (Contributed by NM, 29-Dec-1992.) |
Theorem | exmidd 432 | Law of excluded middle in a context. (Contributed by Mario Carneiro, 9-Feb-2017.) |
Theorem | pm2.1 433 | Theorem *2.1 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) |
Theorem | pm2.13 434 | Theorem *2.13 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm4.62 435 | Theorem *4.62 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm4.66 436 | Theorem *4.66 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm4.63 437 | Theorem *4.63 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
Theorem | imnan 438 | Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.) |
Theorem | imnani 439 | Infer implication from negated conjunction. (Contributed by Mario Carneiro, 28-Sep-2015.) |
Theorem | iman 440 | Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2012.) |
Theorem | annim 441 | Express conjunction in terms of implication. (Contributed by NM, 2-Aug-1994.) |
Theorem | pm4.61 442 | Theorem *4.61 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm4.65 443 | Theorem *4.65 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm4.67 444 | Theorem *4.67 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
Theorem | imp 445 | Importation inference. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) |
Theorem | impcom 446 | Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.) |
Theorem | impd 447 | Importation deduction. (Contributed by NM, 31-Mar-1994.) |
Theorem | imp31 448 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | imp32 449 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
Theorem | ex 450 | Exportation inference. (This theorem used to be labeled "exp" but was changed to "ex" so as not to conflict with the math token "exp", per the June 2006 Metamath spec change.) A translation of natural deduction rule I ( introduction), see natded 27260. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) |
Theorem | expcom 451 | Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.) |
Theorem | expd 452 | Exportation deduction. (Contributed by NM, 20-Aug-1993.) |
Theorem | expdimp 453 | A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.) |
Theorem | expcomd 454 | Deduction form of expcom 451. (Contributed by Alan Sare, 22-Jul-2012.) |
Theorem | expdcom 455 | Commuted form of expd 452. (Contributed by Alan Sare, 18-Mar-2012.) |
Theorem | impancom 456 | Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.) |
Theorem | con3dimp 457 | Variant of con3d 148 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | pm2.01da 458 | Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.) |
Theorem | pm2.18da 459 | Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.) |
Theorem | pm3.3 460 | Theorem *3.3 (Exp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
Theorem | pm3.31 461 | Theorem *3.31 (Imp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
Theorem | impexp 462 | Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
Theorem | pm3.2 463 | Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. See pm3.2im 157 for a version using only implication and negation. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.) |
Theorem | pm3.21 464 | Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.) |
Theorem | pm3.22 465 | Theorem *3.22 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.) |
Theorem | ancom 466 | Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf Lammen, 4-Nov-2012.) |
Theorem | ancomd 467 | Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.) |
Theorem | ancomst 468 | Closed form of ancoms 469. (Contributed by Alan Sare, 31-Dec-2011.) |
Theorem | ancoms 469 | Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.) |
Theorem | ancomsd 470 | Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.) |
Theorem | pm3.2i 471 | Infer conjunction of premises. (Contributed by NM, 21-Jun-1993.) |
Theorem | pm3.43i 472 | Nested conjunction of antecedents. (Contributed by NM, 4-Jan-1993.) |
Theorem | simpl 473 | Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.) |
Theorem | simpli 474 | Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.) |
Theorem | simpld 475 | Deduction eliminating a conjunct. A translation of natural deduction rule EL ( elimination left), see natded 27260. (Contributed by NM, 26-May-1993.) |
Theorem | simplbi 476 | Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.) |
Theorem | simpr 477 | Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.) |
Theorem | simpri 478 | Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.) |
Theorem | simprd 479 | Deduction eliminating a conjunct. (Contributed by NM, 14-May-1993.) A translation of natural deduction rule ER ( elimination right), see natded 27260. (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
Theorem | simprbi 480 | Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.) |
Theorem | adantr 481 | Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.) |
Theorem | adantl 482 | Inference adding a conjunct to the left of an antecedent. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) |
Theorem | adantld 483 | Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.) |
Theorem | adantrd 484 | Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.) |
Theorem | impel 485 | An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.) |
Theorem | mpan9 486 | Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Theorem | syldan 487 | A syllogism deduction with conjoined antecedents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.) |
Theorem | sylan 488 | A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.) |
Theorem | sylanb 489 | A syllogism inference. (Contributed by NM, 18-May-1994.) |
Theorem | sylanbr 490 | A syllogism inference. (Contributed by NM, 18-May-1994.) |
Theorem | sylan2 491 | A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.) |
Theorem | sylan2b 492 | A syllogism inference. (Contributed by NM, 21-Apr-1994.) |
Theorem | sylan2br 493 | A syllogism inference. (Contributed by NM, 21-Apr-1994.) |
Theorem | syl2an 494 | A double syllogism inference. For an implication-only version, see syl2im 40. (Contributed by NM, 31-Jan-1997.) |
Theorem | syl2anr 495 | A double syllogism inference. For an implication-only version, see syl2imc 41. (Contributed by NM, 17-Sep-2013.) |
Theorem | syl2anb 496 | A double syllogism inference. (Contributed by NM, 29-Jul-1999.) |
Theorem | syl2anbr 497 | A double syllogism inference. (Contributed by NM, 29-Jul-1999.) |
Theorem | syland 498 | A syllogism deduction. (Contributed by NM, 15-Dec-2004.) |
Theorem | sylan2d 499 | A syllogism deduction. (Contributed by NM, 15-Dec-2004.) |
Theorem | syl2and 500 | A syllogism deduction. (Contributed by NM, 15-Dec-2004.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |