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

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-1914
  Copyright terms: Public domain < Previous  Next >