Type | Label | Description |
Statement |
|
Theorem | nbn3 701 |
Transfer falsehood via equivalence. (Contributed by NM,
11-Sep-2006.)
|
     |
|
Theorem | 2false 702 |
Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
   |
|
Theorem | 2falsed 703 |
Two falsehoods are equivalent (deduction form). (Contributed by NM,
11-Oct-2013.)
|
         |
|
Theorem | pm5.21ni 704 |
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 705 |
Eliminate an antecedent implied by each side of a biconditional.
(Contributed by NM, 21-May-1999.) (Revised by Mario Carneiro,
31-Jan-2015.)
|
           |
|
Theorem | pm5.21ndd 706 |
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.)
|
         
         |
|
Theorem | pm5.19 707 |
Theorem *5.19 of [WhiteheadRussell] p.
124. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
   |
|
Theorem | pm4.8 708 |
Theorem *4.8 of [WhiteheadRussell] p.
122. This one holds for all
propositions, but compare with pm4.81dc 909 which requires a decidability
condition. (Contributed by NM, 3-Jan-2005.)
|
  
  |
|
1.2.6 Logical disjunction
|
|
Syntax | wo 709 |
Extend wff definition to include disjunction ('or').
|
   |
|
Axiom | ax-io 710 |
Definition of 'or'. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.) Use its alias jaob 711
instead. (New usage is discouraged.)
|
             |
|
Theorem | jaob 711 |
Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell]
p. 121. Alias of ax-io 710. (Contributed by NM, 30-May-1994.) (Revised
by Mario Carneiro, 31-Jan-2015.)
|
             |
|
Theorem | olc 712 |
Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96.
(Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)
|
     |
|
Theorem | orc 713 |
Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104.
(Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)
|
     |
|
Theorem | pm2.67-2 714 |
Slight generalization of Theorem *2.67 of [WhiteheadRussell] p. 107.
(Contributed by NM, 3-Jan-2005.) (Revised by NM, 9-Dec-2012.)
|
         |
|
Theorem | oibabs 715 |
Absorption of disjunction into equivalence. (Contributed by NM,
6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)
|
           |
|
Theorem | pm3.44 716 |
Theorem *3.44 of [WhiteheadRussell] p.
113. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
|
         
   |
|
Theorem | jaoi 717 |
Inference disjoining the antecedents of two implications. (Contributed
by NM, 5-Apr-1994.) (Revised by NM, 31-Jan-2015.)
|
      
  |
|
Theorem | jaod 718 |
Deduction disjoining the antecedents of two implications. (Contributed
by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.)
|
               |
|
Theorem | mpjaod 719 |
Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro,
29-May-2016.)
|
               |
|
Theorem | jaao 720 |
Inference conjoining and disjoining the antecedents of two implications.
(Contributed by NM, 30-Sep-1999.)
|
                 |
|
Theorem | jaoa 721 |
Inference disjoining and conjoining the antecedents of two implications.
(Contributed by Stefan Allan, 1-Nov-2008.)
|
          
      |
|
Theorem | imorr 722 |
Implication in terms of disjunction. One direction of theorem *4.6 of
[WhiteheadRussell] p. 120. The
converse holds for decidable propositions,
as seen at imordc 898. (Contributed by Jim Kingdon, 21-Jul-2018.)
|
       |
|
Theorem | pm2.53 723 |
Theorem *2.53 of [WhiteheadRussell] p.
107. This holds
intuitionistically, although its converse does not (see pm2.54dc 892).
(Contributed by NM, 3-Jan-2005.) (Revised by NM, 31-Jan-2015.)
|
  
    |
|
Theorem | ori 724 |
Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
     |
|
Theorem | ord 725 |
Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
    
    |
|
Theorem | orel1 726 |
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.)
|
       |
|
Theorem | orel2 727 |
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.)
|
       |
|
Theorem | pm1.4 728 |
Axiom *1.4 of [WhiteheadRussell] p.
96. (Contributed by NM, 3-Jan-2005.)
(Revised by NM, 15-Nov-2012.)
|
  
    |
|
Theorem | orcom 729 |
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.)
|
       |
|
Theorem | orcomd 730 |
Commutation of disjuncts in consequent. (Contributed by NM,
2-Dec-2010.)
|
    
    |
|
Theorem | orcoms 731 |
Commutation of disjuncts in antecedent. (Contributed by NM,
2-Dec-2012.)
|
  
      |
|
Theorem | orci 732 |
Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
   |
|
Theorem | olci 733 |
Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
   |
|
Theorem | orcd 734 |
Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)
|
       |
|
Theorem | olcd 735 |
Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.)
(Proof shortened by Wolf Lammen, 3-Oct-2013.)
|
       |
|
Theorem | orcs 736 |
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. (Contributed by NM, 21-Jun-1994.)
|
  
    |
|
Theorem | olcs 737 |
Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.)
(Proof shortened by Wolf Lammen, 3-Oct-2013.)
|
  
    |
|
Theorem | pm2.07 738 |
Theorem *2.07 of [WhiteheadRussell] p.
101. (Contributed by NM,
3-Jan-2005.)
|
     |
|
Theorem | pm2.45 739 |
Theorem *2.45 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
     |
|
Theorem | pm2.46 740 |
Theorem *2.46 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
     |
|
Theorem | pm2.47 741 |
Theorem *2.47 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
       |
|
Theorem | pm2.48 742 |
Theorem *2.48 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
       |
|
Theorem | pm2.49 743 |
Theorem *2.49 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
       |
|
Theorem | pm2.67 744 |
Theorem *2.67 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.) (Revised by NM, 9-Dec-2012.)
|
         |
|
Theorem | biorf 745 |
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.)
|
       |
|
Theorem | biortn 746 |
A wff is equivalent to its negated disjunction with falsehood.
(Contributed by NM, 9-Jul-2012.)
|
       |
|
Theorem | biorfi 747 |
A wff is equivalent to its disjunction with falsehood. (Contributed by
NM, 23-Mar-1995.)
|
     |
|
Theorem | pm2.621 748 |
Theorem *2.621 of [WhiteheadRussell]
p. 107. (Contributed by NM,
3-Jan-2005.) (Revised by NM, 13-Dec-2013.)
|
  
      |
|
Theorem | pm2.62 749 |
Theorem *2.62 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Dec-2013.)
|
  
      |
|
Theorem | imorri 750 |
Infer implication from disjunction. (Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
     |
|
Theorem | pm4.52im 751 |
One direction of theorem *4.52 of [WhiteheadRussell] p. 120. The converse
also holds in classical logic. (Contributed by Jim Kingdon,
27-Jul-2018.)
|
  
    |
|
Theorem | pm4.53r 752 |
One direction of theorem *4.53 of [WhiteheadRussell] p. 120. The converse
also holds in classical logic. (Contributed by Jim Kingdon,
27-Jul-2018.)
|
       |
|
Theorem | ioran 753 |
Negated disjunction in terms of conjunction. This version of DeMorgan's
law is a biconditional for all propositions (not just decidable ones),
unlike oranim 782, anordc 957, or ianordc 900. Compare Theorem *4.56 of
[WhiteheadRussell] p. 120.
(Contributed by NM, 5-Aug-1993.) (Revised by
Mario Carneiro, 31-Jan-2015.)
|
       |
|
Theorem | pm3.14 754 |
Theorem *3.14 of [WhiteheadRussell] p.
111. One direction of De Morgan's
law). The biconditional holds for decidable propositions as seen at
ianordc 900. The converse holds for decidable
propositions, as seen at
pm3.13dc 960. (Contributed by NM, 3-Jan-2005.) (Revised
by Mario
Carneiro, 31-Jan-2015.)
|
       |
|
Theorem | pm3.1 755 |
Theorem *3.1 of [WhiteheadRussell] p.
111. The converse holds for
decidable propositions, as seen at anordc 957. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
  

   |
|
Theorem | jao 756 |
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.)
|
  
    
     |
|
Theorem | pm1.2 757 |
Axiom *1.2 (Taut) of [WhiteheadRussell] p. 96. (Contributed by
NM,
3-Jan-2005.) (Revised by NM, 10-Mar-2013.)
|
  
  |
|
Theorem | oridm 758 |
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.)
|
     |
|
Theorem | pm4.25 759 |
Theorem *4.25 of [WhiteheadRussell] p.
117. (Contributed by NM,
3-Jan-2005.)
|
     |
|
Theorem | orim12i 760 |
Disjoin antecedents and consequents of two premises. (Contributed by
NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
|
      
    |
|
Theorem | orim1i 761 |
Introduce disjunct to both sides of an implication. (Contributed by NM,
6-Jun-1994.)
|
   
     |
|
Theorem | orim2i 762 |
Introduce disjunct to both sides of an implication. (Contributed by NM,
6-Jun-1994.)
|
         |
|
Theorem | orbi2i 763 |
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.)
|
         |
|
Theorem | orbi1i 764 |
Inference adding a right disjunct to both sides of a logical
equivalence. (Contributed by NM, 5-Aug-1993.)
|
         |
|
Theorem | orbi12i 765 |
Infer the disjunction of two equivalences. (Contributed by NM,
5-Aug-1993.)
|
           |
|
Theorem | pm1.5 766 |
Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by
NM,
3-Jan-2005.)
|
    
      |
|
Theorem | or12 767 |
Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by
Wolf Lammen, 14-Nov-2012.)
|
           |
|
Theorem | orass 768 |
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.)
|
           |
|
Theorem | pm2.31 769 |
Theorem *2.31 of [WhiteheadRussell] p.
104. (Contributed by NM,
3-Jan-2005.)
|
    
      |
|
Theorem | pm2.32 770 |
Theorem *2.32 of [WhiteheadRussell] p.
105. (Contributed by NM,
3-Jan-2005.)
|
           |
|
Theorem | or32 771 |
A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof
shortened by Andrew Salmon, 26-Jun-2011.)
|
           |
|
Theorem | or4 772 |
Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)
|
               |
|
Theorem | or42 773 |
Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)
|
               |
|
Theorem | orordi 774 |
Distribution of disjunction over disjunction. (Contributed by NM,
25-Feb-1995.)
|
             |
|
Theorem | orordir 775 |
Distribution of disjunction over disjunction. (Contributed by NM,
25-Feb-1995.)
|
             |
|
Theorem | pm2.3 776 |
Theorem *2.3 of [WhiteheadRussell] p.
104. (Contributed by NM,
3-Jan-2005.)
|
    
      |
|
Theorem | pm2.41 777 |
Theorem *2.41 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
    
    |
|
Theorem | pm2.42 778 |
Theorem *2.42 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
    
    |
|
Theorem | pm2.4 779 |
Theorem *2.4 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
    
    |
|
Theorem | pm4.44 780 |
Theorem *4.44 of [WhiteheadRussell] p.
119. (Contributed by NM,
3-Jan-2005.)
|
       |
|
Theorem | pm4.56 781 |
Theorem *4.56 of [WhiteheadRussell] p.
120. (Contributed by NM,
3-Jan-2005.)
|
       |
|
Theorem | oranim 782 |
Disjunction in terms of conjunction (DeMorgan's law). One direction of
Theorem *4.57 of [WhiteheadRussell] p. 120. The converse
does not hold
intuitionistically but does hold in classical logic. (Contributed by Jim
Kingdon, 25-Jul-2018.)
|
  
    |
|
Theorem | pm4.78i 783 |
Implication distributes over disjunction. One direction of Theorem *4.78
of [WhiteheadRussell] p. 121.
The converse holds in classical logic.
(Contributed by Jim Kingdon, 15-Jan-2018.)
|
       
     |
|
Theorem | mtord 784 |
A modus tollens deduction involving disjunction. (Contributed by Jeff
Hankins, 15-Jul-2009.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
             |
|
Theorem | pm4.45 785 |
Theorem *4.45 of [WhiteheadRussell] p.
119. (Contributed by NM,
3-Jan-2005.)
|
       |
|
Theorem | pm3.48 786 |
Theorem *3.48 of [WhiteheadRussell] p.
114. (Contributed by NM,
28-Jan-1997.) (Revised by NM, 1-Dec-2012.)
|
         
     |
|
Theorem | orim12d 787 |
Disjoin antecedents and consequents in a deduction. (Contributed by NM,
10-May-1994.)
|
                 |
|
Theorem | orim1d 788 |
Disjoin antecedents and consequents in a deduction. (Contributed by NM,
23-Apr-1995.)
|
             |
|
Theorem | orim2d 789 |
Disjoin antecedents and consequents in a deduction. (Contributed by NM,
23-Apr-1995.)
|
             |
|
Theorem | orim2 790 |
Axiom *1.6 (Sum) of [WhiteheadRussell]
p. 97. (Contributed by NM,
3-Jan-2005.)
|
  
        |
|
Theorem | orbi2d 791 |
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.)
|
             |
|
Theorem | orbi1d 792 |
Deduction adding a right disjunct to both sides of a logical
equivalence. (Contributed by NM, 5-Aug-1993.)
|
             |
|
Theorem | orbi1 793 |
Theorem *4.37 of [WhiteheadRussell] p.
118. (Contributed by NM,
3-Jan-2005.)
|
    
      |
|
Theorem | orbi12d 794 |
Deduction joining two equivalences to form equivalence of disjunctions.
(Contributed by NM, 5-Aug-1993.)
|
                 |
|
Theorem | pm5.61 795 |
Theorem *5.61 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.)
|
         |
|
Theorem | jaoian 796 |
Inference disjoining the antecedents of two implications. (Contributed
by NM, 23-Oct-2005.)
|
               |
|
Theorem | jao1i 797 |
Add a disjunct in the antecedent of an implication. (Contributed by
Rodolfo Medina, 24-Sep-2010.)
|
           |
|
Theorem | jaodan 798 |
Deduction disjoining the antecedents of two implications. (Contributed
by NM, 14-Oct-2005.)
|
         
     |
|
Theorem | mpjaodan 799 |
Eliminate a disjunction in a deduction. A translation of natural
deduction rule E (
elimination). (Contributed by Mario
Carneiro, 29-May-2016.)
|
               |
|
Theorem | pm4.77 800 |
Theorem *4.77 of [WhiteheadRussell] p.
121. (Contributed by NM,
3-Jan-2005.)
|
             |