Theorem List for Intuitionistic Logic Explorer - 601-700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | mt2 601 |
A rule similar to modus tollens. (Contributed by NM, 19-Aug-1993.)
(Proof shortened by Wolf Lammen, 10-Sep-2013.)
|
|
|
Theorem | biijust 602 |
Theorem used to justify definition of intuitionistic biconditional
df-bi 115. (Contributed by NM, 24-Nov-2017.)
|
|
|
Theorem | con3 603 |
Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed
by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Feb-2013.)
|
|
|
Theorem | con2 604 |
Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed
by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
|
|
|
Theorem | mt2i 605 |
Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof
shortened by Wolf Lammen, 15-Sep-2012.)
|
|
|
Theorem | notnoti 606 |
Infer double negation. (Contributed by NM, 27-Feb-2008.)
|
|
|
Theorem | pm2.21i 607 |
A contradiction implies anything. Inference from pm2.21 579.
(Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro,
31-Jan-2015.)
|
|
|
Theorem | pm2.24ii 608 |
A contradiction implies anything. Inference from pm2.24 583.
(Contributed by NM, 27-Feb-2008.)
|
|
|
Theorem | nsyld 609 |
A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.)
|
|
|
Theorem | nsyli 610 |
A negated syllogism inference. (Contributed by NM, 3-May-1994.)
|
|
|
Theorem | mth8 611 |
Theorem 8 of [Margaris] p. 60. (Contributed
by NM, 5-Aug-1993.) (Proof
shortened by Josh Purinton, 29-Dec-2000.)
|
|
|
Theorem | jc 612 |
Inference joining the consequents of two premises. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | pm2.51 613 |
Theorem *2.51 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.52 614 |
Theorem *2.52 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | expt 615 |
Exportation theorem expressed with primitive connectives. (Contributed by
NM, 5-Aug-1993.)
|
|
|
Theorem | jarl 616 |
Elimination of a nested antecedent. (Contributed by Wolf Lammen,
10-May-2013.)
|
|
|
Theorem | pm2.65 617 |
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 808, are only valid for decidable propositions.
(Contributed by
NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Mar-2013.)
|
|
|
Theorem | pm2.65d 618 |
Deduction rule for proof by contradiction. (Contributed by NM,
26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.)
|
|
|
Theorem | pm2.65da 619 |
Deduction rule for proof by contradiction. (Contributed by NM,
12-Jun-2014.)
|
|
|
Theorem | mto 620 |
The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof
shortened by Wolf Lammen, 11-Sep-2013.)
|
|
|
Theorem | mtod 621 |
Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof
shortened by Wolf Lammen, 11-Sep-2013.)
|
|
|
Theorem | mtoi 622 |
Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof
shortened by Wolf Lammen, 15-Sep-2012.)
|
|
|
Theorem | mtand 623 |
A modus tollens deduction. (Contributed by Jeff Hankins,
19-Aug-2009.)
|
|
|
Theorem | notbid 624 |
Deduction negating both sides of a logical equivalence. (Contributed by
NM, 21-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | con2b 625 |
Contraposition. Bidirectional version of con2 604.
(Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | notbii 626 |
Negate both sides of a logical equivalence. (Contributed by NM,
5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | mtbi 627 |
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 628 |
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 629 |
A deduction from a biconditional, similar to modus tollens.
(Contributed by NM, 26-Nov-1995.)
|
|
|
Theorem | mtbird 630 |
A deduction from a biconditional, similar to modus tollens.
(Contributed by NM, 10-May-1994.)
|
|
|
Theorem | mtbii 631 |
An inference from a biconditional, similar to modus tollens.
(Contributed by NM, 27-Nov-1995.)
|
|
|
Theorem | mtbiri 632 |
An inference from a biconditional, similar to modus tollens.
(Contributed by NM, 24-Aug-1995.)
|
|
|
Theorem | sylnib 633 |
A mixed syllogism inference from an implication and a biconditional.
(Contributed by Wolf Lammen, 16-Dec-2013.)
|
|
|
Theorem | sylnibr 634 |
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 635 |
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 636 |
A mixed syllogism inference from a biconditional and an implication.
(Contributed by Wolf Lammen, 16-Dec-2013.)
|
|
|
Theorem | xchnxbi 637 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
|
|
Theorem | xchnxbir 638 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
|
|
Theorem | xchbinx 639 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
|
|
Theorem | xchbinxr 640 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
|
|
Theorem | mt2bi 641 |
A false consequent falsifies an antecedent. (Contributed by NM,
19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)
|
|
|
Theorem | mtt 642 |
Modus-tollens-like theorem. (Contributed by NM, 7-Apr-2001.) (Revised by
Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm5.21 643 |
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 644 |
Two propositions are equivalent if they are both false. Closed form of
2false 649. Equivalent to a bi2 128-like version of the xor-connective.
(Contributed by Wolf Lammen, 13-May-2013.) (Revised by Mario Carneiro,
31-Jan-2015.)
|
|
|
Theorem | nbn2 645 |
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 646 |
Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007.)
(Proof shortened by Wolf Lammen, 28-Jan-2013.)
|
|
|
Theorem | nbn 647 |
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 648 |
Transfer falsehood via equivalence. (Contributed by NM,
11-Sep-2006.)
|
|
|
Theorem | 2false 649 |
Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | 2falsed 650 |
Two falsehoods are equivalent (deduction rule). (Contributed by NM,
11-Oct-2013.)
|
|
|
Theorem | pm5.21ni 651 |
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 652 |
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 653 |
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 654 |
Theorem *5.19 of [WhiteheadRussell] p.
124. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm4.8 655 |
Theorem *4.8 of [WhiteheadRussell] p.
122. This one holds for all
propositions, but compare with pm4.81dc 847 which requires a decidability
condition. (Contributed by NM, 3-Jan-2005.)
|
|
|
Theorem | imnan 656 |
Express implication in terms of conjunction. (Contributed by NM,
9-Apr-1994.) (Revised by Mario Carneiro, 1-Feb-2015.)
|
|
|
Theorem | imnani 657 |
Express implication in terms of conjunction. (Contributed by Mario
Carneiro, 28-Sep-2015.)
|
|
|
Theorem | nan 658 |
Theorem to move a conjunct in and out of a negation. (Contributed by NM,
9-Nov-2003.)
|
|
|
Theorem | pm3.24 659 |
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 660 |
Triple negation. (Contributed by Jim Kingdon, 28-Jul-2018.)
|
|
|
1.2.6 Logical disjunction
|
|
Syntax | wo 661 |
Extend wff definition to include disjunction ('or').
|
|
|
Axiom | ax-io 662 |
Definition of 'or'. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.) Use its alias jaob 663
instead. (New usage is discouraged.)
|
|
|
Theorem | jaob 663 |
Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell]
p. 121. Alias of ax-io 662. (Contributed by NM, 30-May-1994.) (Revised
by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | olc 664 |
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 665 |
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 666 |
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 667 |
Theorem *3.44 of [WhiteheadRussell] p.
113. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
|
|
|
Theorem | jaoi 668 |
Inference disjoining the antecedents of two implications. (Contributed
by NM, 5-Apr-1994.) (Revised by NM, 31-Jan-2015.)
|
|
|
Theorem | jaod 669 |
Deduction disjoining the antecedents of two implications. (Contributed
by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.)
|
|
|
Theorem | mpjaod 670 |
Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | jaao 671 |
Inference conjoining and disjoining the antecedents of two implications.
(Contributed by NM, 30-Sep-1999.)
|
|
|
Theorem | jaoa 672 |
Inference disjoining and conjoining the antecedents of two implications.
(Contributed by Stefan Allan, 1-Nov-2008.)
|
|
|
Theorem | pm2.53 673 |
Theorem *2.53 of [WhiteheadRussell] p.
107. This holds
intuitionistically, although its converse does not (see pm2.54dc 823).
(Contributed by NM, 3-Jan-2005.) (Revised by NM, 31-Jan-2015.)
|
|
|
Theorem | ori 674 |
Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | ord 675 |
Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | orel1 676 |
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 677 |
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 678 |
Axiom *1.4 of [WhiteheadRussell] p.
96. (Contributed by NM, 3-Jan-2005.)
(Revised by NM, 15-Nov-2012.)
|
|
|
Theorem | orcom 679 |
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 680 |
Commutation of disjuncts in consequent. (Contributed by NM,
2-Dec-2010.)
|
|
|
Theorem | orcoms 681 |
Commutation of disjuncts in antecedent. (Contributed by NM,
2-Dec-2012.)
|
|
|
Theorem | orci 682 |
Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | olci 683 |
Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | orcd 684 |
Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)
|
|
|
Theorem | olcd 685 |
Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.)
(Proof shortened by Wolf Lammen, 3-Oct-2013.)
|
|
|
Theorem | orcs 686 |
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 687 |
Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.)
(Proof shortened by Wolf Lammen, 3-Oct-2013.)
|
|
|
Theorem | pm2.07 688 |
Theorem *2.07 of [WhiteheadRussell] p.
101. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.45 689 |
Theorem *2.45 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.46 690 |
Theorem *2.46 of [WhiteheadRussell] p.
106. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.47 691 |
Theorem *2.47 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.48 692 |
Theorem *2.48 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.49 693 |
Theorem *2.49 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.67 694 |
Theorem *2.67 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.) (Revised by NM, 9-Dec-2012.)
|
|
|
Theorem | biorf 695 |
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 696 |
A wff is equivalent to its negated disjunction with falsehood.
(Contributed by NM, 9-Jul-2012.)
|
|
|
Theorem | biorfi 697 |
A wff is equivalent to its disjunction with falsehood. (Contributed by
NM, 23-Mar-1995.)
|
|
|
Theorem | pm2.621 698 |
Theorem *2.621 of [WhiteheadRussell]
p. 107. (Contributed by NM,
3-Jan-2005.) (Revised by NM, 13-Dec-2013.)
|
|
|
Theorem | pm2.62 699 |
Theorem *2.62 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Dec-2013.)
|
|
|
Theorem | imorri 700 |
Infer implication from disjunction. (Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|