Home | Intuitionistic Logic ExplorerTheorem List (p. 6 of 21)
| < 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. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.) |

Theorem | an4 502 | Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.) |

Theorem | an42 503 | Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.) |

Theorem | an4s 504 | Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |

Theorem | an42s 505 | Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |

Theorem | anandi 506 | Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.) |

Theorem | anandir 507 | Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.) |

Theorem | anandis 508 | Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.) |

Theorem | anandirs 509 | Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.) |

Theorem | impbida 510 | Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.) |

Theorem | pm3.45 511 | Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |

Theorem | im2anan9 512 | Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.) |

Theorem | im2anan9r 513 | Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.) |

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. (Contributed by NM, 21-May-1994.) |

Theorem | pm3.43 516 | Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 27-Nov-2013.) |

Theorem | jcab 517 | Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 27-Nov-2013.) |

Theorem | pm3.43OLD 518 | Obsolete proof of pm3.43 516 as of 27-Nov-2013 (Contributed by NM, 3-Jan-2005.) |

Theorem | pm4.76 519 | Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) |

Theorem | pm4.38 520 | Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |

Theorem | bi2anan9 521 | Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.) |

Theorem | bi2anan9r 522 | Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996.) |

Theorem | bi2bian9 523 | Deduction joining two biconditionals with different antecedents. (Contributed by NM, 12-May-2004.) |

Theorem | pm5.33 524 | Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |

Theorem | pm5.36 525 | Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |

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. (Contributed by Mario Carneiro, 31-Jan-2015.) |

Axiom | ax-in2 528 | 'Not' elimination. Axiom 5 of 10 for intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.) |

Theorem | pm2.01 529 | Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100. This is valid intuitionistically (in the terminology of [Bauer] p. 482 it is a proof of negation not a proof by contradiction); compare with pm2.18 1955 which is not. (Contributed by Mario Carneiro, 12-May-2015.) |

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. (Contributed by Mario Carneiro, 12-May-2015.) |

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

Theorem | pm2.21d 532 | A contradiction implies anything. Deduction from pm2.21 530. (Contributed by NM, 10-Feb-1996.) |

Theorem | pm2.24 533 | Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |

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

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

Theorem | con2d 536 | A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised by NM, 12-Feb-2013.) |

Theorem | mt2d 537 | Modus tollens deduction. (Contributed by NM, 4-Jul-1994.) |

Theorem | nsyl3 538 | A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) (Revised by NM, 13-Jun-2013.) |

Theorem | con2i 539 | A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.) |

Theorem | nsyl 540 | A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.) |

Theorem | notnot1 541 | Adding double negation. Theorem *2.12 of [WhiteheadRussell] p. 101. This one holds intuitionistically, but its converse, notnot2 1962, does not. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.) |

Theorem | con3d 542 | A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.) |

Theorem | con3i 543 | A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.) |

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

Theorem | con3and 545 | Variant of con3d 542 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |

Theorem | pm3.2im 546 | In classical logic, this is just a restatement of pm3.2 124. In intuitionistic logic, it still holds, but is weaker than pm3.2. (Contributed by Mario Carneiro, 12-May-2015.) |

Theorem | expi 547 | An exportation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) |

Theorem | pm2.65i 548 | Inference rule for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |

Theorem | mt2 549 | A rule similar to modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.) |

Theorem | biijust 550 | Theorem used to justify definition of intuitionistic biconditional df-bi 108. (Contributed by NM, 24-Nov-2017.) |

Theorem | con3 551 | Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Feb-2013.) |

Theorem | con2 552 | Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2013.) |

Theorem | mt2i 553 | Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |

Theorem | notnoti 554 | Infer double negation. (Contributed by NM, 27-Feb-2008.) |

Theorem | pm2.21i 555 | A contradiction implies anything. Inference from pm2.21 530. (Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | pm2.24ii 556 | A contradiction implies anything. Inference from pm2.24 533. (Contributed by NM, 27-Feb-2008.) |

Theorem | nsyld 557 | A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.) |

Theorem | nsyli 558 | A negated syllogism inference. (Contributed by NM, 3-May-1994.) |

Theorem | mth8 559 | Theorem 8 of [Margaris] p. 60. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |

Theorem | jc 560 | Inference joining the consequents of two premises. (Contributed by NM, 5-Aug-1993.) |

Theorem | pm2.51 561 | Theorem *2.51 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |

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

Theorem | expt 563 | Exportation theorem expressed with primitive connectives. (Contributed by NM, 5-Aug-1993.) |

Theorem | jarl 564 | Elimination of a nested antecedent. Although it is a kind of reversal of inference ja 1960 it holds intuitionistically, while ja 1960 does not. (Contributed by Wolf Lammen, 10-May-2013.) |

Theorem | pm2.65 565 | Theorem *2.65 of [WhiteheadRussell] p. 107. Proof by contradiction. Proofs, such as this one, which assume a proposition, here , derive a contradiction, and therefore conclude , are valid intuitionistically (and can be called "proof of negation", for example by [Bauer] p. 482). By contrast, proofs which assume , derive a contradiction, and conclude , such as condandc 746, are only valid for decidable propositions. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Mar-2013.) |

Theorem | pm2.65d 566 | Deduction rule for proof by contradiction. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.) |

Theorem | pm2.65da 567 | Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.) |

Theorem | mto 568 | The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |

Theorem | mtod 569 | Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |

Theorem | mtoi 570 | Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |

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

Theorem | notbid 572 | Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | con2b 573 | Contraposition. Bidirectional version of con2 552. (Contributed by NM, 5-Aug-1993.) |

Theorem | notbii 574 | Negate both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | mtbi 575 | An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |

Theorem | mtbir 576 | An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.) |

Theorem | mtbid 577 | A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.) |

Theorem | mtbird 578 | A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.) |

Theorem | mtbii 579 | An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.) |

Theorem | mtbiri 580 | An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.) |

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

Theorem | sylnibr 582 | 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 583 | 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 584 | A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.) |

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

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

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

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

Theorem | mt2bi 589 | A false consequent falsifies an antecedent. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.) |

Theorem | mtt 590 | Modus-tollens-like theorem. (Contributed by NM, 7-Apr-2001.) (Revised by Mario Carneiro, 31-Jan-2015.) |

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

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

Theorem | nbn2 593 | 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 594 | Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007.) (Proof shortened by Wolf Lammen, 28-Jan-2013.) |

Theorem | nbn 595 | The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2013.) |

Theorem | nbn3 596 | Transfer falsehood via equivalence. (Contributed by NM, 11-Sep-2006.) |

Theorem | 2false 597 | Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 31-Jan-2015.) |

Theorem | 2falsed 598 | Two falsehoods are equivalent (deduction rule). (Contributed by NM, 11-Oct-2013.) |

Theorem | pm5.21ni 599 | Two propositions implying a false one are equivalent. (Contributed by NM, 16-Feb-1996.) (Proof shortened by Wolf Lammen, 19-May-2013.) |

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

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |