Theorem List for Intuitionistic Logic Explorer - 601-700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | sylnib 601 |
A mixed syllogism inference from an implication and a biconditional.
(Contributed by Wolf Lammen, 16-Dec-2013.)
|
|
|
Theorem | sylnibr 602 |
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.)
|
|
|
Theorem | sylnbi 603 |
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.)
|
|
|
Theorem | sylnbir 604 |
A mixed syllogism inference from a biconditional and an implication.
(Contributed by Wolf Lammen, 16-Dec-2013.)
|
|
|
Theorem | xchnxbi 605 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
|
|
Theorem | xchnxbir 606 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
|
|
Theorem | xchbinx 607 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
|
|
Theorem | xchbinxr 608 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
|
|
Theorem | mt2bi 609 |
A false consequent falsifies an antecedent. (Contributed by NM,
19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)
|
|
|
Theorem | mtt 610 |
Modus-tollens-like theorem. (Contributed by NM, 7-Apr-2001.) (Revised by
Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm5.21 611 |
Two propositions are equivalent if they are both false. Theorem *5.21 of
[WhiteheadRussell] p. 124.
(Contributed by NM, 21-May-1994.) (Revised by
Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm5.21im 612 |
Two propositions are equivalent if they are both false. Closed form of
2false 617. Equivalent to a bi2 121-like version of the xor-connective.
(Contributed by Wolf Lammen, 13-May-2013.) (Revised by Mario Carneiro,
31-Jan-2015.)
|
|
|
Theorem | nbn2 613 |
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.)
|
|
|
Theorem | bibif 614 |
Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007.)
(Proof shortened by Wolf Lammen, 28-Jan-2013.)
|
|
|
Theorem | nbn 615 |
The negation of a wff is equivalent to the wff's equivalence to
falsehood. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf
Lammen, 3-Oct-2013.)
|
|
|
Theorem | nbn3 616 |
Transfer falsehood via equivalence. (Contributed by NM,
11-Sep-2006.)
|
|
|
Theorem | 2false 617 |
Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | 2falsed 618 |
Two falsehoods are equivalent (deduction rule). (Contributed by NM,
11-Oct-2013.)
|
|
|
Theorem | pm5.21ni 619 |
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 620 |
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 621 |
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 622 |
Theorem *5.19 of [WhiteheadRussell] p.
124. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm4.8 623 |
Theorem *4.8 of [WhiteheadRussell] p.
122. This one holds for all
propositions, but compare with pm4.81dc 814 which requires a decidability
condition. (Contributed by NM, 3-Jan-2005.)
|
|
|
Theorem | imnan 624 |
Express implication in terms of conjunction. (Contributed by NM,
9-Apr-1994.) (Revised by Mario Carneiro, 1-Feb-2015.)
|
|
|
Theorem | imnani 625 |
Express implication in terms of conjunction. (Contributed by Mario
Carneiro, 28-Sep-2015.)
|
|
|
Theorem | nan 626 |
Theorem to move a conjunct in and out of a negation. (Contributed by NM,
9-Nov-2003.)
|
|
|
Theorem | pm3.24 627 |
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.)
|
|
|
Theorem | notnotnot 628 |
Triple negation. (Contributed by Jim Kingdon, 28-Jul-2018.)
|
|
|
1.2.6 Logical disjunction
|
|
Syntax | wo 629 |
Extend wff definition to include disjunction ('or').
|
|
|
Axiom | ax-io 630 |
Definition of 'or'. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | jaob 631 |
Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell]
p. 121. (Contributed by NM, 30-May-1994.) (Revised by Mario Carneiro,
31-Jan-2015.)
|
|
|
Theorem | olc 632 |
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 633 |
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 634 |
Slight generalization of Theorem *2.67 of [WhiteheadRussell] p. 107.
(Contributed by NM, 3-Jan-2005.) (Revised by NM, 9-Dec-2012.)
|
|
|
Theorem | pm3.44 635 |
Theorem *3.44 of [WhiteheadRussell] p.
113. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
|
|
|
Theorem | jaoi 636 |
Inference disjoining the antecedents of two implications. (Contributed
by NM, 5-Apr-1994.) (Revised by NM, 31-Jan-2015.)
|
|
|
Theorem | jaod 637 |
Deduction disjoining the antecedents of two implications. (Contributed
by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.)
|
|
|
Theorem | mpjaod 638 |
Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | jaao 639 |
Inference conjoining and disjoining the antecedents of two implications.
(Contributed by NM, 30-Sep-1999.)
|
|
|
Theorem | jaoa 640 |
Inference disjoining and conjoining the antecedents of two implications.
(Contributed by Stefan Allan, 1-Nov-2008.)
|
|
|
Theorem | pm2.53 641 |
Theorem *2.53 of [WhiteheadRussell] p.
107. This holds
intuitionistically, although its converse does not (see pm2.54dc 790).
(Contributed by NM, 3-Jan-2005.) (Revised by NM, 31-Jan-2015.)
|
|
|
Theorem | ori 642 |
Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | ord 643 |
Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | orel1 644 |
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 645 |
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 646 |
Axiom *1.4 of [WhiteheadRussell] p.
96. (Contributed by NM, 3-Jan-2005.)
(Revised by NM, 15-Nov-2012.)
|
|
|
Theorem | orcom 647 |
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 648 |
Commutation of disjuncts in consequent. (Contributed by NM,
2-Dec-2010.)
|
|
|
Theorem | orcoms 649 |
Commutation of disjuncts in antecedent. (Contributed by NM,
2-Dec-2012.)
|
|
|
Theorem | orci 650 |
Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | olci 651 |
Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | orcd 652 |
Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)
|
|
|
Theorem | olcd 653 |
Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.)
(Proof shortened by Wolf Lammen, 3-Oct-2013.)
|
|
|
Theorem | orcs 654 |
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 655 |
Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.)
(Proof shortened by Wolf Lammen, 3-Oct-2013.)
|
|
|
Theorem | pm2.07 656 |
Theorem *2.07 of [WhiteheadRussell] p.
101. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.45 657 |
Theorem *2.45 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.46 658 |
Theorem *2.46 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.47 659 |
Theorem *2.47 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.48 660 |
Theorem *2.48 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.49 661 |
Theorem *2.49 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.67 662 |
Theorem *2.67 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.) (Revised by NM, 9-Dec-2012.)
|
|
|
Theorem | biorf 663 |
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 664 |
A wff is equivalent to its negated disjunction with falsehood.
(Contributed by NM, 9-Jul-2012.)
|
|
|
Theorem | biorfi 665 |
A wff is equivalent to its disjunction with falsehood. (Contributed by
NM, 23-Mar-1995.)
|
|
|
Theorem | pm2.621 666 |
Theorem *2.621 of [WhiteheadRussell]
p. 107. (Contributed by NM,
3-Jan-2005.) (Revised by NM, 13-Dec-2013.)
|
|
|
Theorem | pm2.62 667 |
Theorem *2.62 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Dec-2013.)
|
|
|
Theorem | imorri 668 |
Infer implication from disjunction. (Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | ioran 669 |
Negated disjunction in terms of conjunction. This version of DeMorgan's
law is a biconditional for all propositions (not just decidable ones),
unlike oranim 807, anordc 863, or ianordc 799. Compare Theorem *4.56 of
[WhiteheadRussell] p. 120.
(Contributed by NM, 5-Aug-1993.) (Revised by
Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm3.14 670 |
Theorem *3.14 of [WhiteheadRussell] p.
111. One direction of De Morgan's
law). The biconditional holds for decidable propositions as seen at
ianordc 799. The converse holds for decidable
propositions, as seen at
pm3.13dc 866. (Contributed by NM, 3-Jan-2005.) (Revised
by Mario
Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm3.1 671 |
Theorem *3.1 of [WhiteheadRussell] p.
111. The converse holds for
decidable propositions, as seen at anordc 863. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | jao 672 |
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 673 |
Axiom *1.2 (Taut) of [WhiteheadRussell] p. 96. (Contributed by
NM,
3-Jan-2005.) (Revised by NM, 10-Mar-2013.)
|
|
|
Theorem | oridm 674 |
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 675 |
Theorem *4.25 of [WhiteheadRussell] p.
117. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | orim12i 676 |
Disjoin antecedents and consequents of two premises. (Contributed by
NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
|
|
|
Theorem | orim1i 677 |
Introduce disjunct to both sides of an implication. (Contributed by NM,
6-Jun-1994.)
|
|
|
Theorem | orim2i 678 |
Introduce disjunct to both sides of an implication. (Contributed by NM,
6-Jun-1994.)
|
|
|
Theorem | orbi2i 679 |
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 680 |
Inference adding a right disjunct to both sides of a logical
equivalence. (Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | orbi12i 681 |
Infer the disjunction of two equivalences. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | pm1.5 682 |
Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by
NM,
3-Jan-2005.)
|
|
|
Theorem | or12 683 |
Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by
Wolf Lammen, 14-Nov-2012.)
|
|
|
Theorem | orass 684 |
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 685 |
Theorem *2.31 of [WhiteheadRussell] p.
104. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.32 686 |
Theorem *2.32 of [WhiteheadRussell] p.
105. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | or32 687 |
A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof
shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | or4 688 |
Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)
|
|
|
Theorem | or42 689 |
Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)
|
|
|
Theorem | orordi 690 |
Distribution of disjunction over disjunction. (Contributed by NM,
25-Feb-1995.)
|
|
|
Theorem | orordir 691 |
Distribution of disjunction over disjunction. (Contributed by NM,
25-Feb-1995.)
|
|
|
Theorem | pm2.3 692 |
Theorem *2.3 of [WhiteheadRussell] p.
104. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.41 693 |
Theorem *2.41 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.42 694 |
Theorem *2.42 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.4 695 |
Theorem *2.4 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm4.44 696 |
Theorem *4.44 of [WhiteheadRussell] p.
119. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | mtord 697 |
A modus tollens deduction involving disjunction. (Contributed by Jeff
Hankins, 15-Jul-2009.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm4.45 698 |
Theorem *4.45 of [WhiteheadRussell] p.
119. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm3.48 699 |
Theorem *3.48 of [WhiteheadRussell] p.
114. (Contributed by NM,
28-Jan-1997.) (Revised by NM, 1-Dec-2012.)
|
|
|
Theorem | orim12d 700 |
Disjoin antecedents and consequents in a deduction. (Contributed by NM,
10-May-1994.)
|
|