Home | Intuitionistic Logic ExplorerTheorem List (p. 6 of 20)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | anabss3 501 | Absorption of antecedent into conjunction. (The proof was shortened by Wolf Lammen, 1-Jan-2013.) |

Theorem | an4 502 | Rearrangement of 4 conjuncts. |

Theorem | an42 503 | Rearrangement of 4 conjuncts. |

Theorem | an4s 504 | Inference rearranging 4 conjuncts in antecedent. |

Theorem | an42s 505 | Inference rearranging 4 conjuncts in antecedent. |

Theorem | anandi 506 | Distribution of conjunction over conjunction. |

Theorem | anandir 507 | Distribution of conjunction over conjunction. |

Theorem | anandis 508 | Inference that undistributes conjunction in the antecedent. |

Theorem | anandirs 509 | Inference that undistributes conjunction in the antecedent. |

Theorem | impbida 510 | Deduce an equivalence from two implications. |

Theorem | pm3.45 511 | Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. |

Theorem | im2anan9 512 | Deduction joining nested implications to form implication of conjunctions. |

Theorem | im2anan9r 513 | Deduction joining nested implications to form implication of conjunctions. |

Theorem | anim12dan 514 | Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.) |

Theorem | pm5.1 515 | Two propositions are equivalent if they are both true. Theorem *5.1 of [WhiteheadRussell] p. 123. |

Theorem | pm3.43 516 | Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. |

Theorem | jcab 517 | Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121. (The proof was shortened by Wolf Lammen, 27-Nov-2013.) |

Theorem | pm3.43OLD 518 | Obsolete proof of pm3.43 516 as of 27-Nov-2013 |

Theorem | pm4.76 519 | Theorem *4.76 of [WhiteheadRussell] p. 121. |

Theorem | pm4.38 520 | Theorem *4.38 of [WhiteheadRussell] p. 118. |

Theorem | bi2anan9 521 | Deduction joining two equivalences to form equivalence of conjunctions. |

Theorem | bi2anan9r 522 | Deduction joining two equivalences to form equivalence of conjunctions. |

Theorem | bi2bian9 523 | Deduction joining two biconditionals with different antecedents. |

Theorem | pm5.33 524 | Theorem *5.33 of [WhiteheadRussell] p. 125. |

Theorem | pm5.36 525 | Theorem *5.36 of [WhiteheadRussell] p. 125. |

Theorem | bianabs 526 | Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.) |

1.2.5 Logical negation
(intuitionistic) | ||

Axiom | ax-in1 527 | 'Not' introduction. Axiom 4 of 10 for intuitionistic logic. |

Axiom | ax-in2 528 | 'Not' elimination. Axiom 5 of 10 for intuitionistic logic. |

Theorem | pm2.01 529 | Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100. (The proof was shortened by O'Cat, 21-Nov-2008.) (The proof was shortened by Wolf Lammen, 31-Oct-2012.) |

Theorem | pm2.21 530 | From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. (The proof was shortened by Wolf Lammen, 14-Sep-2012.) |

Theorem | pm2.01d 531 | Deduction based on reductio ad absurdum. (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | pm2.21d 532 | A contradiction implies anything. Deduction from pm2.21 530. |

Theorem | pm2.24 533 | Theorem *2.24 of [WhiteheadRussell] p. 104. |

Theorem | pm2.24d 534 | Deduction version of pm2.24 533. (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | pm2.24i 535 | Inference version of pm2.24 533. (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | con2d 536 | A contraposition deduction. |

Theorem | mt2d 537 | Modus tollens deduction. |

Theorem | nsyl3 538 | A negated syllogism inference. |

Theorem | con2i 539 | A contraposition inference. (The proof was shortened by O'Cat, 28-Nov-2008.) (The proof was shortened by Wolf Lammen, 13-Jun-2013.) |

Theorem | nsyl 540 | A negated syllogism inference. (The proof was shortened by Wolf Lammen, 2-Mar-2013.) |

Theorem | notnot1 541 | Converse of double negation. Theorem *2.12 of [WhiteheadRussell] p. 101. (The proof was shortened by Wolf Lammen, 2-Mar-2013.) |

Theorem | con3d 542 | A contraposition deduction. |

Theorem | con3i 543 | A contraposition inference. (The proof was shortened by Wolf Lammen, 20-Jun-2013.) |

Theorem | con3rr3 544 | Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.) |

Theorem | pm3.2im 545 | Theorem *3.2 of [WhiteheadRussell] p. 111, expressed with primitive connectives. (The proof was shortened by Josh Purinton, 29-Dec-2000.) |

Theorem | expi 546 | An exportation inference. (The proof was shortened by O'Cat, 28-Nov-2008.) |

Theorem | pm2.65i 547 | Inference rule for proof by contradiction. (The proof was shortened by Wolf Lammen, 11-Sep-2013.) |

Theorem | mt2 548 | A rule similar to modus tollens. (The proof was shortened by Wolf Lammen, 10-Sep-2013.) |

Theorem | bijust 549 | Theorem used to justify definition of biconditional df-bi 109. (The proof was shortened by Josh Purinton, 29-Dec-2000.) |

Theorem | con3 550 | Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. (The proof was shortened by Wolf Lammen, 13-Feb-2013.) |

Theorem | con2 551 | Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (The proof was shortened by Wolf Lammen, 12-Feb-2013.) |

Theorem | mt2i 552 | Modus tollens inference. (The proof was shortened by Wolf Lammen, 15-Sep-2012.) |

Theorem | notnoti 553 | Infer double negation. |

Theorem | pm2.21i 554 | A contradiction implies anything. Inference from pm2.21 530. (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | pm2.24ii 555 | A contradiction implies anything. Inference from pm2.24 533. |

Theorem | nsyld 556 | A negated syllogism deduction. |

Theorem | nsyli 557 | A negated syllogism inference. |

Theorem | mth8 558 | Theorem 8 of [Margaris] p. 60. (The proof was shortened by Josh Purinton, 29-Dec-2000.) |

Theorem | jc 559 | Inference joining the consequents of two premises. |

Theorem | pm2.51 560 | Theorem *2.51 of [WhiteheadRussell] p. 107. |

Theorem | pm2.52 561 | Theorem *2.52 of [WhiteheadRussell] p. 107. (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | expt 562 | Exportation theorem expressed with primitive connectives. |

Theorem | jarl 563 | Elimination of a nested antecedent as a kind of reversal of inference ja 738. (Contributed by Wolf Lammen, 10-May-2013.) |

Theorem | pm2.65 564 | Theorem *2.65 of [WhiteheadRussell] p. 107. Proof by contradiction. (The proof was shortened by Wolf Lammen, 8-Mar-2013.) |

Theorem | pm2.65d 565 | Deduction rule for proof by contradiction. (The proof was shortened by Wolf Lammen, 26-May-2013.) |

Theorem | pm2.65da 566 | Deduction rule for proof by contradiction. |

Theorem | mto 567 | The rule of modus tollens. (The proof was shortened by Wolf Lammen, 11-Sep-2013.) |

Theorem | mtod 568 | Modus tollens deduction. (The proof was shortened by Wolf Lammen, 11-Sep-2013.) |

Theorem | mtoi 569 | Modus tollens inference. (The proof was shortened by Wolf Lammen, 15-Sep-2012.) |

Theorem | mtand 570 | A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.) |

Theorem | notbid 571 | Deduction negating both sides of a logical equivalence. (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | con2b 572 | Contraposition. Bidirectional version of con2 551. |

Theorem | notbii 573 | Negate both sides of a logical equivalence. (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | mtbi 574 | An inference from a biconditional, related to modus tollens. (The proof was shortened by Wolf Lammen, 25-Oct-2012.) |

Theorem | mtbir 575 | An inference from a biconditional, related to modus tollens. (The proof was shortened by Wolf Lammen, 14-Oct-2012.) |

Theorem | mtbid 576 | A deduction from a biconditional, similar to modus tollens. |

Theorem | mtbird 577 | A deduction from a biconditional, similar to modus tollens. |

Theorem | mtbii 578 | An inference from a biconditional, similar to modus tollens. |

Theorem | mtbiri 579 | An inference from a biconditional, similar to modus tollens. |

Theorem | sylnib 580 | A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.) |

Theorem | sylnibr 581 | A mixed syllogism inference from an implication and a biconditional. Useful for substituting an consequent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.) |

Theorem | sylnbi 582 | A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.) |

Theorem | sylnbir 583 | A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.) |

Theorem | xchnxbi 584 | Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |

Theorem | xchnxbir 585 | Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |

Theorem | xchbinx 586 | Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |

Theorem | xchbinxr 587 | Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |

Theorem | mt2bi 588 | A false consequent falsifies an antecedent. (The proof was shortened by Wolf Lammen, 12-Nov-2012.) |

Theorem | mtt 589 | Modus-tollens-like theorem. (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | pm5.21 590 | Two propositions are equivalent if they are both false. Theorem *5.21 of [WhiteheadRussell] p. 124. (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | pm5.21im 591 | Two propositions are equivalent if they are both false. Closed form of 2false 596. Equivalent to a bi2 120-like version of the xor-connective. (Contributed by Wolf Lammen, 13-May-2013.) (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | nbn2 592 | The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by Juha Arpiainen, 19-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | bibif 593 | Transfer negation via an equivalence. (The proof was shortened by Wolf Lammen, 28-Jan-2013.) |

Theorem | nbn 594 | The negation of a wff is equivalent to the wff's equivalence to falsehood. (The proof was shortened by Wolf Lammen, 3-Oct-2013.) |

Theorem | nbn3 595 | Transfer falsehood via equivalence. |

Theorem | 2false 596 | Two falsehoods are equivalent. (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | 2falsed 597 | Two falsehoods are equivalent (deduction rule). |

Theorem | pm5.21ni 598 | Two propositions implying a false one are equivalent. (The proof was shortened by Wolf Lammen, 19-May-2013.) |

Theorem | pm5.21nii 599 | Eliminate an antecedent implied by each side of a biconditional. (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | pm5.21ndd 600 | Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Revised by Mario Carneiro, 31-Jan-2015.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |