HomeHome Intuitionistic Logic Explorer
Theorem List (p. 7 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 - 601-700   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorempm5.21ndd 601 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.)
   &       &       =>   
 
Theorempm5.19 602 Theorem *5.19 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
 
Theorempm4.8 603 Theorem *4.8 of [WhiteheadRussell] p. 122. This one is valid in intuitionistic logic, whereas pm4.81 2074 is not. (Contributed by NM, 3-Jan-2005.)
 
Theoremimnan 604 Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.) (Revised by Mario Carneiro, 1-Feb-2015.)
 
Theoremnan 605 Theorem to move a conjunct in and out of a negation. (Contributed by NM, 9-Nov-2003.)
 
Theorempm3.24 606 Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who call it the "law of contradiction"). (Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro, 2-Feb-2015.)
 
1.2.6  Logical disjunction
 
Syntaxwo 607 Extend wff definition to include disjunction ('or').
 
Axiomax-io 608 Definition of 'or'. Axiom 6 of 10 for intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
 
Theoremjaob 609 Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
 
Theoremolc 610 Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)
 
Theoremorc 611 Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)
 
Theorempm2.67-2 612 Slight generalization of Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 9-Dec-2012.)
 
Theorempm3.44 613 Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
 
Theoremjaoi 614 Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.) (Revised by NM, 31-Jan-2015.)
   &       =>   
 
Theoremjaod 615 Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.)
   &       =>   
 
Theoremjaao 616 Inference conjoining and disjoining the antecedents of two implications. (Contributed by NM, 30-Sep-1999.)
   &       =>   
 
Theoremjaoa 617 Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008.)
   &       =>   
 
Theorempm2.53 618 Theorem *2.53 of [WhiteheadRussell] p. 107. This holds intuitionistically, although its converse, pm2.54 1972, does not. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 31-Jan-2015.)
 
Theoremori 619 Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
   =>   
 
Theoremord 620 Deduce implication from disjunction. (Contributed by NM, 18-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
   =>   
 
Theoremorel1 621 Elimination of disjunction by denial of a disjunct. Theorem *2.55 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 21-Jul-2012.)
 
Theoremorel2 622 Elimination of disjunction by denial of a disjunct. Theorem *2.56 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 5-Apr-2013.)
 
Theorempm1.4 623 Axiom *1.4 of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 15-Nov-2012.)
 
Theoremorcom 624 Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Nov-2012.)
 
Theoremorcomd 625 Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.)
   =>   
 
Theoremorcoms 626 Commutation of disjuncts in antecedent. (Contributed by NM, 2-Dec-2012.)
   =>   
 
Theoremorci 627 Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.)
   =>   
 
Theoremolci 628 Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.)
   =>   
 
Theoremorcd 629 Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)
   =>   
 
Theoremolcd 630 Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
   =>   
 
Theoremorcs 631 Deduction eliminating disjunct. Notational convention: We sometimes suffix with "s" the label of an inference that manipulates an antecedent, leaving the consequent unchanged. The "s" means that the inference eliminates the need for a syllogism (syl 13) -type inference in a proof. (Contributed by NM, 21-Jun-1994.)
   =>   
 
Theoremolcs 632 Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
   =>   
 
Theorempm2.07 633 Theorem *2.07 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.45 634 Theorem *2.45 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.46 635 Theorem *2.46 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.47 636 Theorem *2.47 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.48 637 Theorem *2.48 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.49 638 Theorem *2.49 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.67 639 Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 9-Dec-2012.)
 
Theorembiorf 640 A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of [WhiteheadRussell] p. 121. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)
 
Theorembiortn 641 A wff is equivalent to its negated disjunction with falsehood. (Contributed by NM, 9-Jul-2012.)
 
Theorembiorfi 642 A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.)
   =>   
 
Theorempm2.621 643 Theorem *2.621 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 13-Dec-2013.)
 
Theorempm2.62 644 Theorem *2.62 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Dec-2013.)
 
Theoremimorri 645 Infer implication from disjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by Mario Carneiro, 31-Jan-2015.)
   =>   
 
Theoremioran 646 Negated disjunction in terms of conjunction. This version of DeMorgan's law holds for all propositions (not just decidable ones), unlike oran 2077, anordc 823, or ianordc 768. Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
 
Theorempm3.14 647 Theorem *3.14 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
 
Theorempm3.1 648 Theorem *3.1 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
 
Theoremjao 649 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.)
 
Theorempm1.2 650 Axiom *1.2 (Taut) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 10-Mar-2013.)
 
Theoremoridm 651 Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 16-Apr-2011.) (Proof shortened by Wolf Lammen, 10-Mar-2013.)
 
Theorempm4.25 652 Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
 
Theoremorim12i 653 Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
   &       =>   
 
Theoremorim1i 654 Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
   =>   
 
Theoremorim2i 655 Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
   =>   
 
Theoremorbi2i 656 Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.)
   =>   
 
Theoremorbi1i 657 Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremorbi12i 658 Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.)
   &       =>   
 
Theorempm1.5 659 Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.)
 
Theoremor12 660 Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
 
Theoremorass 661 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.)
 
Theorempm2.31 662 Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.32 663 Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.)
 
Theoremor32 664 A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
 
Theoremor4 665 Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)
 
Theoremor42 666 Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)
 
Theoremorordi 667 Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
 
Theoremorordir 668 Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
 
Theorempm2.3 669 Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.41 670 Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.42 671 Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.4 672 Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
 
Theorempm4.44 673 Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
 
Theoremmtord 674 A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.) (Revised by Mario Carneiro, 31-Jan-2015.)
   &       &       =>   
 
Theorempm4.45 675 Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
 
Theorempm3.48 676 Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.) (Revised by NM, 1-Dec-2012.)
 
Theoremorim12d 677 Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)
   &       =>   
 
Theoremorim1d 678 Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
   =>   
 
Theoremorim2d 679 Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
   =>   
 
Theoremorim2 680 Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.)
 
Theoremorbi2d 681 Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
   =>   
 
Theoremorbi1d 682 Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremorbi1 683 Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
 
Theoremorbi12d 684 Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)
   &       =>   
 
Theorempm5.61 685 Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.)
 
Theoremjaoian 686 Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.)
   &       =>   
 
Theoremjaodan 687 Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)
   &       =>   
 
Theorempm4.77 688 Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.63 689 Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.64 690 Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
 
Theorempm5.53 691 Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.38 692 Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
 
Theorempm2.36 693 Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
 
Theorempm2.37 694 Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
 
Theorempm2.73 695 Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
 
Theorempm2.74 696 Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2015.)
 
Theorempm2.76 697 Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
 
Theorempm2.75 698 Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.)
 
Theorempm2.8 699 Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2015.)
 
Theorempm2.81 700 Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600601-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 >