Home | Metamath
Proof Explorer Theorem List (p. 6 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 | biimpa 501 | Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
Theorem | biimpar 502 | Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
Theorem | biimpac 503 | Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
Theorem | biimparc 504 | Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
Theorem | animorl 505 | Conjunction implies disjunction with one common formula (1/4). (Contributed by BJ, 4-Oct-2019.) |
Theorem | animorr 506 | Conjunction implies disjunction with one common formula (2/4). (Contributed by BJ, 4-Oct-2019.) |
Theorem | animorlr 507 | Conjunction implies disjunction with one common formula (3/4). (Contributed by BJ, 4-Oct-2019.) |
Theorem | animorrl 508 | Conjunction implies disjunction with one common formula (4/4). (Contributed by BJ, 4-Oct-2019.) |
Theorem | ianor 509 | Negated conjunction in terms of disjunction (De Morgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | anor 510 | Conjunction in terms of disjunction (De Morgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 3-Nov-2012.) |
Theorem | ioran 511 | Negated disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Theorem | pm4.52 512 | Theorem *4.52 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.) |
Theorem | pm4.53 513 | Theorem *4.53 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm4.54 514 | Theorem *4.54 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.) |
Theorem | pm4.55 515 | Theorem *4.55 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm4.56 516 | Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
Theorem | oran 517 | Disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Theorem | pm4.57 518 | Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm3.1 519 | Theorem *3.1 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm3.11 520 | Theorem *3.11 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm3.12 521 | Theorem *3.12 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm3.13 522 | Theorem *3.13 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm3.14 523 | Theorem *3.14 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
Theorem | iba 524 | Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.) |
Theorem | ibar 525 | Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.) |
Theorem | biantru 526 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 26-May-1993.) |
Theorem | biantrur 527 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.) |
Theorem | biantrud 528 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.) |
Theorem | biantrurd 529 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Theorem | mpbirand 530 | Detach truth from conjunction in biconditional. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Theorem | jaao 531 | Inference conjoining and disjoining the antecedents of two implications. (Contributed by NM, 30-Sep-1999.) |
Theorem | jaoa 532 | Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008.) |
Theorem | pm3.44 533 | Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
Theorem | jao 534 | Disjunction of antecedents. Compare Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 4-Apr-2013.) |
Theorem | pm1.2 535 | Axiom *1.2 of [WhiteheadRussell] p. 96, which they call "Taut". (Contributed by NM, 3-Jan-2005.) |
Theorem | oridm 536 | Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) (Proof shortened by Andrew Salmon, 16-Apr-2011.) (Proof shortened by Wolf Lammen, 10-Mar-2013.) |
Theorem | pm4.25 537 | Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) |
Theorem | orim12i 538 | Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.) |
Theorem | orim1i 539 | Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
Theorem | orim2i 540 | Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
Theorem | orbi2i 541 | Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.) |
Theorem | orbi1i 542 | Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) |
Theorem | orbi12i 543 | Infer the disjunction of two equivalences. (Contributed by NM, 3-Jan-1993.) |
Theorem | pm1.5 544 | Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) |
Theorem | or12 545 | Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.) |
Theorem | orass 546 | Associative law for disjunction. Theorem *4.33 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | pm2.31 547 | Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.32 548 | Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.) |
Theorem | or32 549 | A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | or4 550 | Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.) |
Theorem | or42 551 | Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.) |
Theorem | orordi 552 | Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.) |
Theorem | orordir 553 | Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.) |
Theorem | jca 554 | Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). Equivalent to the natural deduction rule I ( introduction), see natded 27260. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |
Theorem | jcad 555 | Deduction conjoining the consequents of two implications. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.) |
Theorem | jca2 556 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
Theorem | jca31 557 | Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.) |
Theorem | jca32 558 | Join three consequents. (Contributed by FL, 1-Aug-2009.) |
Theorem | jcai 559 | Deduction replacing implication with conjunction. (Contributed by NM, 15-Jul-1993.) |
Theorem | jctil 560 | Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.) |
Theorem | jctir 561 | Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.) |
Theorem | jccir 562 | Inference conjoining a consequent of a consequent to the right of the consequent in an implication. See also ex-natded5.3i 27266. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by AV, 20-Aug-2019.) |
Theorem | jccil 563 | Inference conjoining a consequent of a consequent to the left of the consequent in an implication. Remark: One can also prove this theorem using syl 17 and jca 554 (as done in jccir 562), which would be 4 bytes shorter, but one step longer than the current proof. (Proof modification is discouraged.) (Contributed by AV, 20-Aug-2019.) |
Theorem | jctl 564 | Inference conjoining a theorem to the left of a consequent. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.) |
Theorem | jctr 565 | Inference conjoining a theorem to the right of a consequent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.) |
Theorem | jctild 566 | Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.) |
Theorem | jctird 567 | Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.) |
Theorem | syl6an 568 | A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.) |
Theorem | ancl 569 | Conjoin antecedent to left of consequent. (Contributed by NM, 15-Aug-1994.) |
Theorem | anclb 570 | Conjoin antecedent to left of consequent. Theorem *4.7 of [WhiteheadRussell] p. 120. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
Theorem | pm5.42 571 | Theorem *5.42 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
Theorem | ancr 572 | Conjoin antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.) |
Theorem | ancrb 573 | Conjoin antecedent to right of consequent. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
Theorem | ancli 574 | Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.) |
Theorem | ancri 575 | Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.) |
Theorem | ancld 576 | Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.) |
Theorem | ancrd 577 | Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.) |
Theorem | anc2l 578 | Conjoin antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 14-Jul-2013.) |
Theorem | anc2r 579 | Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) |
Theorem | anc2li 580 | Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.) |
Theorem | anc2ri 581 | Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.) |
Theorem | pm3.41 582 | Theorem *3.41 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm3.42 583 | Theorem *3.42 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm3.4 584 | Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113. (Contributed by NM, 31-Jul-1995.) |
Theorem | pm4.45im 585 | Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.) |
Theorem | anim12d 586 | Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.) |
Theorem | anim12d1 587 | Variant of anim12d 586 where the second implication does not depend on the antecedent. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
Theorem | anim1d 588 | Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.) |
Theorem | anim2d 589 | Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993.) |
Theorem | anim12i 590 | Conjoin antecedents and consequents of two premises. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.) |
Theorem | anim12ci 591 | Variant of anim12i 590 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | anim1i 592 | Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.) |
Theorem | anim2i 593 | Introduce conjunct to both sides of an implication. (Contributed by NM, 3-Jan-1993.) |
Theorem | anim12ii 594 | Conjoin antecedents and consequents in a deduction. (Contributed by NM, 11-Nov-2007.) (Proof shortened by Wolf Lammen, 19-Jul-2013.) |
Theorem | prth 595 | Conjoin antecedents and consequents of two premises. This is the closed theorem form of anim12d 586. Theorem *3.47 of [WhiteheadRussell] p. 113. It was proved by Leibniz, and it evidently pleased him enough to call it praeclarum theorema (splendid theorem). (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
Theorem | pm2.3 596 | Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.41 597 | Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.42 598 | Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.4 599 | Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.65da 600 | Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |