Theorem List for Intuitionistic Logic Explorer - 701-800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | pm1.4 701 |
Axiom *1.4 of [WhiteheadRussell] p.
96. (Contributed by NM, 3-Jan-2005.)
(Revised by NM, 15-Nov-2012.)
|
|
|
Theorem | orcom 702 |
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 703 |
Commutation of disjuncts in consequent. (Contributed by NM,
2-Dec-2010.)
|
|
|
Theorem | orcoms 704 |
Commutation of disjuncts in antecedent. (Contributed by NM,
2-Dec-2012.)
|
|
|
Theorem | orci 705 |
Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | olci 706 |
Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | orcd 707 |
Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)
|
|
|
Theorem | olcd 708 |
Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.)
(Proof shortened by Wolf Lammen, 3-Oct-2013.)
|
|
|
Theorem | orcs 709 |
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 710 |
Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.)
(Proof shortened by Wolf Lammen, 3-Oct-2013.)
|
|
|
Theorem | pm2.07 711 |
Theorem *2.07 of [WhiteheadRussell] p.
101. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.45 712 |
Theorem *2.45 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.46 713 |
Theorem *2.46 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.47 714 |
Theorem *2.47 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.48 715 |
Theorem *2.48 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.49 716 |
Theorem *2.49 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.67 717 |
Theorem *2.67 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.) (Revised by NM, 9-Dec-2012.)
|
|
|
Theorem | biorf 718 |
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 719 |
A wff is equivalent to its negated disjunction with falsehood.
(Contributed by NM, 9-Jul-2012.)
|
|
|
Theorem | biorfi 720 |
A wff is equivalent to its disjunction with falsehood. (Contributed by
NM, 23-Mar-1995.)
|
|
|
Theorem | pm2.621 721 |
Theorem *2.621 of [WhiteheadRussell]
p. 107. (Contributed by NM,
3-Jan-2005.) (Revised by NM, 13-Dec-2013.)
|
|
|
Theorem | pm2.62 722 |
Theorem *2.62 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Dec-2013.)
|
|
|
Theorem | imorri 723 |
Infer implication from disjunction. (Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm4.52im 724 |
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 725 |
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 726 |
Negated disjunction in terms of conjunction. This version of DeMorgan's
law is a biconditional for all propositions (not just decidable ones),
unlike oranim 755, anordc 925, or ianordc 869. Compare Theorem *4.56 of
[WhiteheadRussell] p. 120.
(Contributed by NM, 5-Aug-1993.) (Revised by
Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm3.14 727 |
Theorem *3.14 of [WhiteheadRussell] p.
111. One direction of De Morgan's
law). The biconditional holds for decidable propositions as seen at
ianordc 869. The converse holds for decidable
propositions, as seen at
pm3.13dc 928. (Contributed by NM, 3-Jan-2005.) (Revised
by Mario
Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm3.1 728 |
Theorem *3.1 of [WhiteheadRussell] p.
111. The converse holds for
decidable propositions, as seen at anordc 925. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | jao 729 |
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 730 |
Axiom *1.2 (Taut) of [WhiteheadRussell] p. 96. (Contributed by
NM,
3-Jan-2005.) (Revised by NM, 10-Mar-2013.)
|
|
|
Theorem | oridm 731 |
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 732 |
Theorem *4.25 of [WhiteheadRussell] p.
117. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | orim12i 733 |
Disjoin antecedents and consequents of two premises. (Contributed by
NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
|
|
|
Theorem | orim1i 734 |
Introduce disjunct to both sides of an implication. (Contributed by NM,
6-Jun-1994.)
|
|
|
Theorem | orim2i 735 |
Introduce disjunct to both sides of an implication. (Contributed by NM,
6-Jun-1994.)
|
|
|
Theorem | orbi2i 736 |
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 737 |
Inference adding a right disjunct to both sides of a logical
equivalence. (Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | orbi12i 738 |
Infer the disjunction of two equivalences. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | pm1.5 739 |
Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by
NM,
3-Jan-2005.)
|
|
|
Theorem | or12 740 |
Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by
Wolf Lammen, 14-Nov-2012.)
|
|
|
Theorem | orass 741 |
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 742 |
Theorem *2.31 of [WhiteheadRussell] p.
104. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.32 743 |
Theorem *2.32 of [WhiteheadRussell] p.
105. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | or32 744 |
A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof
shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | or4 745 |
Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)
|
|
|
Theorem | or42 746 |
Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)
|
|
|
Theorem | orordi 747 |
Distribution of disjunction over disjunction. (Contributed by NM,
25-Feb-1995.)
|
|
|
Theorem | orordir 748 |
Distribution of disjunction over disjunction. (Contributed by NM,
25-Feb-1995.)
|
|
|
Theorem | pm2.3 749 |
Theorem *2.3 of [WhiteheadRussell] p.
104. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.41 750 |
Theorem *2.41 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.42 751 |
Theorem *2.42 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.4 752 |
Theorem *2.4 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm4.44 753 |
Theorem *4.44 of [WhiteheadRussell] p.
119. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm4.56 754 |
Theorem *4.56 of [WhiteheadRussell] p.
120. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | oranim 755 |
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 756 |
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 757 |
A modus tollens deduction involving disjunction. (Contributed by Jeff
Hankins, 15-Jul-2009.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm4.45 758 |
Theorem *4.45 of [WhiteheadRussell] p.
119. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm3.48 759 |
Theorem *3.48 of [WhiteheadRussell] p.
114. (Contributed by NM,
28-Jan-1997.) (Revised by NM, 1-Dec-2012.)
|
|
|
Theorem | orim12d 760 |
Disjoin antecedents and consequents in a deduction. (Contributed by NM,
10-May-1994.)
|
|
|
Theorem | orim1d 761 |
Disjoin antecedents and consequents in a deduction. (Contributed by NM,
23-Apr-1995.)
|
|
|
Theorem | orim2d 762 |
Disjoin antecedents and consequents in a deduction. (Contributed by NM,
23-Apr-1995.)
|
|
|
Theorem | orim2 763 |
Axiom *1.6 (Sum) of [WhiteheadRussell]
p. 97. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | orbi2d 764 |
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 765 |
Deduction adding a right disjunct to both sides of a logical
equivalence. (Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | orbi1 766 |
Theorem *4.37 of [WhiteheadRussell] p.
118. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | orbi12d 767 |
Deduction joining two equivalences to form equivalence of disjunctions.
(Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | pm5.61 768 |
Theorem *5.61 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.)
|
|
|
Theorem | jaoian 769 |
Inference disjoining the antecedents of two implications. (Contributed
by NM, 23-Oct-2005.)
|
|
|
Theorem | jao1i 770 |
Add a disjunct in the antecedent of an implication. (Contributed by
Rodolfo Medina, 24-Sep-2010.)
|
|
|
Theorem | jaodan 771 |
Deduction disjoining the antecedents of two implications. (Contributed
by NM, 14-Oct-2005.)
|
|
|
Theorem | mpjaodan 772 |
Eliminate a disjunction in a deduction. A translation of natural
deduction rule E (
elimination). (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | pm4.77 773 |
Theorem *4.77 of [WhiteheadRussell] p.
121. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.63 774 |
Theorem *2.63 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.64 775 |
Theorem *2.64 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm5.53 776 |
Theorem *5.53 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.38 777 |
Theorem *2.38 of [WhiteheadRussell] p.
105. (Contributed by NM,
6-Mar-2008.)
|
|
|
Theorem | pm2.36 778 |
Theorem *2.36 of [WhiteheadRussell] p.
105. (Contributed by NM,
6-Mar-2008.)
|
|
|
Theorem | pm2.37 779 |
Theorem *2.37 of [WhiteheadRussell] p.
105. (Contributed by NM,
6-Mar-2008.)
|
|
|
Theorem | pm2.73 780 |
Theorem *2.73 of [WhiteheadRussell] p.
108. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.74 781 |
Theorem *2.74 of [WhiteheadRussell] p.
108. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm2.76 782 |
Theorem *2.76 of [WhiteheadRussell] p.
108. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm2.75 783 |
Theorem *2.75 of [WhiteheadRussell] p.
108. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.)
|
|
|
Theorem | pm2.8 784 |
Theorem *2.8 of [WhiteheadRussell] p.
108. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm2.81 785 |
Theorem *2.81 of [WhiteheadRussell] p.
108. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.82 786 |
Theorem *2.82 of [WhiteheadRussell] p.
108. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm3.2ni 787 |
Infer negated disjunction of negated premises. (Contributed by NM,
4-Apr-1995.)
|
|
|
Theorem | orabs 788 |
Absorption of redundant internal disjunct. Compare Theorem *4.45 of
[WhiteheadRussell] p. 119.
(Contributed by NM, 5-Aug-1993.) (Proof
shortened by Wolf Lammen, 28-Feb-2014.)
|
|
|
Theorem | oranabs 789 |
Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton,
23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.)
|
|
|
Theorem | ordi 790 |
Distributive law for disjunction. Theorem *4.41 of [WhiteheadRussell]
p. 119. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro,
31-Jan-2015.)
|
|
|
Theorem | ordir 791 |
Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
|
|
|
Theorem | andi 792 |
Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell]
p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf
Lammen, 5-Jan-2013.)
|
|
|
Theorem | andir 793 |
Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
|
|
|
Theorem | orddi 794 |
Double distributive law for disjunction. (Contributed by NM,
12-Aug-1994.)
|
|
|
Theorem | anddi 795 |
Double distributive law for conjunction. (Contributed by NM,
12-Aug-1994.)
|
|
|
Theorem | pm4.39 796 |
Theorem *4.39 of [WhiteheadRussell] p.
118. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm4.72 797 |
Implication in terms of biconditional and disjunction. Theorem *4.72 of
[WhiteheadRussell] p. 121.
(Contributed by NM, 30-Aug-1993.) (Proof
shortened by Wolf Lammen, 30-Jan-2013.)
|
|
|
Theorem | pm5.16 798 |
Theorem *5.16 of [WhiteheadRussell] p.
124. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | biort 799 |
A wff is disjoined with truth is true. (Contributed by NM,
23-May-1999.)
|
|
|
1.2.7 Stable propositions
|
|
Syntax | wstab 800 |
Extend wff definition to include stability.
|
STAB |