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