HomeHome Intuitionistic Logic Explorer
Theorem List (p. 6 of 21)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 501-600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremanabss3 501 Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
   =>   
 
Theoreman4 502 Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
 
Theoreman42 503 Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
 
Theoreman4s 504 Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
   =>   
 
Theoreman42s 505 Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
   =>   
 
Theoremanandi 506 Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
 
Theoremanandir 507 Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.)
 
Theoremanandis 508 Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
   =>   
 
Theoremanandirs 509 Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
   =>   
 
Theoremimpbida 510 Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
   &       =>   
 
Theorempm3.45 511 Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
 
Theoremim2anan9 512 Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
   &       =>   
 
Theoremim2anan9r 513 Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
   &       =>   
 
Theoremanim12dan 514 Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)
   &       =>   
 
Theorempm5.1 515 Two propositions are equivalent if they are both true. Theorem *5.1 of [WhiteheadRussell] p. 123. (Contributed by NM, 21-May-1994.)
 
Theorempm3.43 516 Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 27-Nov-2013.)
 
Theoremjcab 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.)
 
Theorempm3.43OLD 518 Obsolete proof of pm3.43 516 as of 27-Nov-2013 (Contributed by NM, 3-Jan-2005.)
 
Theorempm4.76 519 Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
 
Theorempm4.38 520 Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
 
Theorembi2anan9 521 Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)
   &       =>   
 
Theorembi2anan9r 522 Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996.)
   &       =>   
 
Theorembi2bian9 523 Deduction joining two biconditionals with different antecedents. (Contributed by NM, 12-May-2004.)
   &       =>   
 
Theorempm5.33 524 Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
 
Theorempm5.36 525 Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
 
Theorembianabs 526 Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.)
   =>   
 
1.2.5  Logical negation (intuitionistic)
 
Axiomax-in1 527 'Not' introduction. Axiom 4 of 10 for intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
 
Axiomax-in2 528 'Not' elimination. Axiom 5 of 10 for intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
 
Theorempm2.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.)
 
Theorempm2.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.)
 
Theorempm2.01d 531 Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
   =>   
 
Theorempm2.21d 532 A contradiction implies anything. Deduction from pm2.21 530. (Contributed by NM, 10-Feb-1996.)
   =>   
 
Theorempm2.24 533 Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.24d 534 Deduction version of pm2.24 533. (Contributed by NM, 30-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2015.)
   =>   
 
Theorempm2.24i 535 Inference version of pm2.24 533. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 31-Jan-2015.)
   =>   
 
Theoremcon2d 536 A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised by NM, 12-Feb-2013.)
   =>   
 
Theoremmt2d 537 Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
   &       =>   
 
Theoremnsyl3 538 A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) (Revised by NM, 13-Jun-2013.)
   &       =>   
 
Theoremcon2i 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.)
   =>   
 
Theoremnsyl 540 A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
   &       =>   
 
Theoremnotnot1 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.)
 
Theoremcon3d 542 A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.)
   =>   
 
Theoremcon3i 543 A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)
   =>   
 
Theoremcon3rr3 544 Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.)
   =>   
 
Theoremcon3and 545 Variant of con3d 542 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
   =>   
 
Theorempm3.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.)
 
Theoremexpi 547 An exportation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.)
   =>   
 
Theorempm2.65i 548 Inference rule for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
   &       =>   
 
Theoremmt2 549 A rule similar to modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.)
   &       =>   
 
Theorembiijust 550 Theorem used to justify definition of intuitionistic biconditional df-bi 108. (Contributed by NM, 24-Nov-2017.)
 
Theoremcon3 551 Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Feb-2013.)
 
Theoremcon2 552 Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
 
Theoremmt2i 553 Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
   &       =>   
 
Theoremnotnoti 554 Infer double negation. (Contributed by NM, 27-Feb-2008.)
   =>   
 
Theorempm2.21i 555 A contradiction implies anything. Inference from pm2.21 530. (Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
   =>   
 
Theorempm2.24ii 556 A contradiction implies anything. Inference from pm2.24 533. (Contributed by NM, 27-Feb-2008.)
   &       =>   
 
Theoremnsyld 557 A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.)
   &       =>   
 
Theoremnsyli 558 A negated syllogism inference. (Contributed by NM, 3-May-1994.)
   &       =>   
 
Theoremmth8 559 Theorem 8 of [Margaris] p. 60. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
 
Theoremjc 560 Inference joining the consequents of two premises. (Contributed by NM, 5-Aug-1993.)
   &       =>   
 
Theorempm2.51 561 Theorem *2.51 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.52 562 Theorem *2.52 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
 
Theoremexpt 563 Exportation theorem expressed with primitive connectives. (Contributed by NM, 5-Aug-1993.)
 
Theoremjarl 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.)
 
Theorempm2.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.)
 
Theorempm2.65d 566 Deduction rule for proof by contradiction. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.)
   &       =>   
 
Theorempm2.65da 567 Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.)
   &       =>   
 
Theoremmto 568 The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
   &       =>   
 
Theoremmtod 569 Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
   &       =>   
 
Theoremmtoi 570 Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
   &       =>   
 
Theoremmtand 571 A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
   &       =>   
 
Theoremnotbid 572 Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
   =>   
 
Theoremcon2b 573 Contraposition. Bidirectional version of con2 552. (Contributed by NM, 5-Aug-1993.)
 
Theoremnotbii 574 Negate both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
   =>   
 
Theoremmtbi 575 An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
   &       =>   
 
Theoremmtbir 576 An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.)
   &       =>   
 
Theoremmtbid 577 A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)
   &       =>   
 
Theoremmtbird 578 A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.)
   &       =>   
 
Theoremmtbii 579 An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.)
   &       =>   
 
Theoremmtbiri 580 An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.)
   &       =>   
 
Theoremsylnib 581 A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)
   &       =>   
 
Theoremsylnibr 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.)
   &       =>   
 
Theoremsylnbi 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.)
   &       =>   
 
Theoremsylnbir 584 A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.)
   &       =>   
 
Theoremxchnxbi 585 Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
   &       =>   
 
Theoremxchnxbir 586 Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
   &       =>   
 
Theoremxchbinx 587 Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
   &       =>   
 
Theoremxchbinxr 588 Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
   &       =>   
 
Theoremmt2bi 589 A false consequent falsifies an antecedent. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)
   =>   
 
Theoremmtt 590 Modus-tollens-like theorem. (Contributed by NM, 7-Apr-2001.) (Revised by Mario Carneiro, 31-Jan-2015.)
 
Theorempm5.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.)
 
Theorempm5.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.)
 
Theoremnbn2 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.)
 
Theorembibif 594 Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007.) (Proof shortened by Wolf Lammen, 28-Jan-2013.)
 
Theoremnbn 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.)
   =>   
 
Theoremnbn3 596 Transfer falsehood via equivalence. (Contributed by NM, 11-Sep-2006.)
   =>   
 
Theorem2false 597 Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
   &       =>   
 
Theorem2falsed 598 Two falsehoods are equivalent (deduction rule). (Contributed by NM, 11-Oct-2013.)
   &       =>   
 
Theorempm5.21ni 599 Two propositions implying a false one are equivalent. (Contributed by NM, 16-Feb-1996.) (Proof shortened by Wolf Lammen, 19-May-2013.)
   &       =>   
 
Theorempm5.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 >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2099
  Copyright terms: Public domain < Previous  Next >