Theorem List for Intuitionistic Logic Explorer - 601-700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | con2i 601 |
A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen,
13-Jun-2013.)
|
|
|
Theorem | nsyl 602 |
A negated syllogism inference. (Contributed by NM, 31-Dec-1993.)
(Proof shortened by Wolf Lammen, 2-Mar-2013.)
|
|
|
Theorem | notnot 603 |
Double negation introduction. Theorem *2.12 of [WhiteheadRussell] p. 101.
The converse need not hold. It holds exactly for stable propositions (by
definition, see df-stab 801) and in particular for decidable propositions
(see notnotrdc 813). See also notnotnot 608. (Contributed by NM,
28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
|
|
|
Theorem | notnotd 604 |
Deduction associated with notnot 603 and notnoti 619. (Contributed by
Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf
Lammen, 27-Mar-2021.)
|
|
|
Theorem | con3d 605 |
A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised
by NM, 31-Jan-2015.)
|
|
|
Theorem | con3i 606 |
A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by Wolf Lammen, 20-Jun-2013.)
|
|
|
Theorem | con3rr3 607 |
Rotate through consequent right. (Contributed by Wolf Lammen,
3-Nov-2013.)
|
|
|
Theorem | notnotnot 608 |
Triple negation is equivalent to negation. (Contributed by Jim Kingdon,
28-Jul-2018.)
|
|
|
Theorem | con3dimp 609 |
Variant of con3d 605 with importation. (Contributed by Jonathan
Ben-Naim,
3-Jun-2011.)
|
|
|
Theorem | pm2.01da 610 |
Deduction based on reductio ad absurdum. (Contributed by Mario
Carneiro, 9-Feb-2017.)
|
|
|
Theorem | pm3.2im 611 |
In classical logic, this is just a restatement of pm3.2 138. In
intuitionistic logic, it still holds, but is weaker than pm3.2.
(Contributed by Mario Carneiro, 12-May-2015.)
|
|
|
Theorem | expi 612 |
An exportation inference. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by O'Cat, 28-Nov-2008.)
|
|
|
Theorem | pm2.65i 613 |
Inference for proof by contradiction. (Contributed by NM, 18-May-1994.)
(Proof shortened by Wolf Lammen, 11-Sep-2013.)
|
|
|
Theorem | mt2 614 |
A rule similar to modus tollens. (Contributed by NM, 19-Aug-1993.)
(Proof shortened by Wolf Lammen, 10-Sep-2013.)
|
|
|
Theorem | biijust 615 |
Theorem used to justify definition of intuitionistic biconditional
df-bi 116. (Contributed by NM, 24-Nov-2017.)
|
|
|
Theorem | con3 616 |
Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed
by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Feb-2013.)
|
|
|
Theorem | con2 617 |
Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed
by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
|
|
|
Theorem | mt2i 618 |
Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof
shortened by Wolf Lammen, 15-Sep-2012.)
|
|
|
Theorem | notnoti 619 |
Infer double negation. (Contributed by NM, 27-Feb-2008.)
|
|
|
Theorem | pm2.21i 620 |
A contradiction implies anything. Inference from pm2.21 591.
(Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro,
31-Jan-2015.)
|
|
|
Theorem | pm2.24ii 621 |
A contradiction implies anything. Inference from pm2.24 595.
(Contributed by NM, 27-Feb-2008.)
|
|
|
Theorem | nsyld 622 |
A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.)
|
|
|
Theorem | nsyli 623 |
A negated syllogism inference. (Contributed by NM, 3-May-1994.)
|
|
|
Theorem | mth8 624 |
Theorem 8 of [Margaris] p. 60. (Contributed
by NM, 5-Aug-1993.) (Proof
shortened by Josh Purinton, 29-Dec-2000.)
|
|
|
Theorem | jc 625 |
Inference joining the consequents of two premises. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | jcn 626 |
Inference joining the consequents of two premises. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
|
|
Theorem | conax1 627 |
Contrapositive of ax-1 6. (Contributed by BJ, 28-Oct-2023.)
|
|
|
Theorem | conax1k 628 |
Weakening of conax1 627. General instance of pm2.51 629 and of pm2.52 630.
(Contributed by BJ, 28-Oct-2023.)
|
|
|
Theorem | pm2.51 629 |
Theorem *2.51 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.52 630 |
Theorem *2.52 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | expt 631 |
Exportation theorem pm3.3 259 (closed form of ex 114)
expressed with
primitive connectives. (Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | jarl 632 |
Elimination of a nested antecedent. (Contributed by Wolf Lammen,
10-May-2013.)
|
|
|
Theorem | pm2.65 633 |
Theorem *2.65 of [WhiteheadRussell] p.
107. Proof by contradiction.
Proofs, such as this one, which assume a proposition, here , derive
a contradiction, and therefore conclude , are valid
intuitionistically (and can be called "proof of negation", for
example by
Section 1.2 of [Bauer] p. 482). By
contrast, proofs which assume
, derive a
contradiction, and conclude , such as
condandc 851, are only valid for decidable propositions.
(Contributed by
NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Mar-2013.)
|
|
|
Theorem | pm2.65d 634 |
Deduction for proof by contradiction. (Contributed by NM, 26-Jun-1994.)
(Proof shortened by Wolf Lammen, 26-May-2013.)
|
|
|
Theorem | pm2.65da 635 |
Deduction for proof by contradiction. (Contributed by NM,
12-Jun-2014.)
|
|
|
Theorem | mto 636 |
The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof
shortened by Wolf Lammen, 11-Sep-2013.)
|
|
|
Theorem | mtod 637 |
Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof
shortened by Wolf Lammen, 11-Sep-2013.)
|
|
|
Theorem | mtoi 638 |
Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof
shortened by Wolf Lammen, 15-Sep-2012.)
|
|
|
Theorem | mtand 639 |
A modus tollens deduction. (Contributed by Jeff Hankins,
19-Aug-2009.)
|
|
|
Theorem | notbi 640 |
Equivalence property for negation. Closed form. (Contributed by BJ,
27-Jan-2020.)
|
|
|
Theorem | notbid 641 |
Equivalence property for negation. Deduction form. (Contributed by NM,
21-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | notbii 642 |
Equivalence property for negation. Inference form. (Contributed by NM,
5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | con2b 643 |
Contraposition. Bidirectional version of con2 617.
(Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | mtbi 644 |
An inference from a biconditional, related to modus tollens.
(Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen,
25-Oct-2012.)
|
|
|
Theorem | mtbir 645 |
An inference from a biconditional, related to modus tollens.
(Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen,
14-Oct-2012.)
|
|
|
Theorem | mtbid 646 |
A deduction from a biconditional, similar to modus tollens.
(Contributed by NM, 26-Nov-1995.)
|
|
|
Theorem | mtbird 647 |
A deduction from a biconditional, similar to modus tollens.
(Contributed by NM, 10-May-1994.)
|
|
|
Theorem | mtbii 648 |
An inference from a biconditional, similar to modus tollens.
(Contributed by NM, 27-Nov-1995.)
|
|
|
Theorem | mtbiri 649 |
An inference from a biconditional, similar to modus tollens.
(Contributed by NM, 24-Aug-1995.)
|
|
|
Theorem | sylnib 650 |
A mixed syllogism inference from an implication and a biconditional.
(Contributed by Wolf Lammen, 16-Dec-2013.)
|
|
|
Theorem | sylnibr 651 |
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 652 |
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 653 |
A mixed syllogism inference from a biconditional and an implication.
(Contributed by Wolf Lammen, 16-Dec-2013.)
|
|
|
Theorem | xchnxbi 654 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
|
|
Theorem | xchnxbir 655 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
|
|
Theorem | xchbinx 656 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
|
|
Theorem | xchbinxr 657 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
|
|
Theorem | mt2bi 658 |
A false consequent falsifies an antecedent. (Contributed by NM,
19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)
|
|
|
Theorem | mtt 659 |
Modus-tollens-like theorem. (Contributed by NM, 7-Apr-2001.) (Revised by
Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | annimim 660 |
Express conjunction in terms of implication. One direction of Theorem
*4.61 of [WhiteheadRussell] p.
120. The converse holds for decidable
propositions, as can be seen at annimdc 906. (Contributed by Jim Kingdon,
24-Dec-2017.)
|
|
|
Theorem | pm4.65r 661 |
One direction of Theorem *4.65 of [WhiteheadRussell] p. 120. The converse
holds in classical logic. (Contributed by Jim Kingdon, 28-Jul-2018.)
|
|
|
Theorem | imanim 662 |
Express implication in terms of conjunction. The converse only holds
given a decidability condition; see imandc 859. (Contributed by Jim
Kingdon, 24-Dec-2017.)
|
|
|
Theorem | pm3.37 663 |
Theorem *3.37 (Transp) of [WhiteheadRussell] p. 112. (Contributed
by NM,
3-Jan-2005.)
|
|
|
Theorem | imnan 664 |
Express implication in terms of conjunction. (Contributed by NM,
9-Apr-1994.) (Revised by Mario Carneiro, 1-Feb-2015.)
|
|
|
Theorem | imnani 665 |
Express implication in terms of conjunction. (Contributed by Mario
Carneiro, 28-Sep-2015.)
|
|
|
Theorem | nan 666 |
Theorem to move a conjunct in and out of a negation. (Contributed by NM,
9-Nov-2003.)
|
|
|
Theorem | pm3.24 667 |
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 | pm4.15 668 |
Theorem *4.15 of [WhiteheadRussell] p.
117. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)
|
|
|
Theorem | pm5.21 669 |
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 670 |
Two propositions are equivalent if they are both false. Closed form of
2false 675. Equivalent to a bi2 129-like version of the xor-connective.
(Contributed by Wolf Lammen, 13-May-2013.) (Revised by Mario Carneiro,
31-Jan-2015.)
|
|
|
Theorem | nbn2 671 |
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 672 |
Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007.)
(Proof shortened by Wolf Lammen, 28-Jan-2013.)
|
|
|
Theorem | nbn 673 |
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 674 |
Transfer falsehood via equivalence. (Contributed by NM,
11-Sep-2006.)
|
|
|
Theorem | 2false 675 |
Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | 2falsed 676 |
Two falsehoods are equivalent (deduction form). (Contributed by NM,
11-Oct-2013.)
|
|
|
Theorem | pm5.21ni 677 |
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 678 |
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 679 |
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 680 |
Theorem *5.19 of [WhiteheadRussell] p.
124. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm4.8 681 |
Theorem *4.8 of [WhiteheadRussell] p.
122. This one holds for all
propositions, but compare with pm4.81dc 878 which requires a decidability
condition. (Contributed by NM, 3-Jan-2005.)
|
|
|
1.2.6 Logical disjunction
|
|
Syntax | wo 682 |
Extend wff definition to include disjunction ('or').
|
|
|
Axiom | ax-io 683 |
Definition of 'or'. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.) Use its alias jaob 684
instead. (New usage is discouraged.)
|
|
|
Theorem | jaob 684 |
Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell]
p. 121. Alias of ax-io 683. (Contributed by NM, 30-May-1994.) (Revised
by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | olc 685 |
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 686 |
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 687 |
Slight generalization of Theorem *2.67 of [WhiteheadRussell] p. 107.
(Contributed by NM, 3-Jan-2005.) (Revised by NM, 9-Dec-2012.)
|
|
|
Theorem | oibabs 688 |
Absorption of disjunction into equivalence. (Contributed by NM,
6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)
|
|
|
Theorem | pm3.44 689 |
Theorem *3.44 of [WhiteheadRussell] p.
113. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
|
|
|
Theorem | jaoi 690 |
Inference disjoining the antecedents of two implications. (Contributed
by NM, 5-Apr-1994.) (Revised by NM, 31-Jan-2015.)
|
|
|
Theorem | jaod 691 |
Deduction disjoining the antecedents of two implications. (Contributed
by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.)
|
|
|
Theorem | mpjaod 692 |
Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | jaao 693 |
Inference conjoining and disjoining the antecedents of two implications.
(Contributed by NM, 30-Sep-1999.)
|
|
|
Theorem | jaoa 694 |
Inference disjoining and conjoining the antecedents of two implications.
(Contributed by Stefan Allan, 1-Nov-2008.)
|
|
|
Theorem | imorr 695 |
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 867. (Contributed by Jim Kingdon, 21-Jul-2018.)
|
|
|
Theorem | pm2.53 696 |
Theorem *2.53 of [WhiteheadRussell] p.
107. This holds
intuitionistically, although its converse does not (see pm2.54dc 861).
(Contributed by NM, 3-Jan-2005.) (Revised by NM, 31-Jan-2015.)
|
|
|
Theorem | ori 697 |
Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | ord 698 |
Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | orel1 699 |
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 700 |
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.)
|
|