Theorem List for Intuitionistic Logic Explorer - 501-600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | an13s 501 |
Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|
|
|
Theorem | an32s 502 |
Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
|
|
|
Theorem | ancom1s 503 |
Inference commuting a nested conjunction in antecedent. (Contributed by
NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|
|
|
Theorem | an31s 504 |
Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|
|
|
Theorem | anass1rs 505 |
Commutative-associative law for conjunction in an antecedent.
(Contributed by Jeff Madsen, 19-Jun-2011.)
|
|
|
Theorem | anabs1 506 |
Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995.)
(Proof shortened by Wolf Lammen, 16-Nov-2013.)
|
|
|
Theorem | anabs5 507 |
Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.)
(Proof shortened by Wolf Lammen, 9-Dec-2012.)
|
|
|
Theorem | anabs7 508 |
Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.)
(Proof shortened by Wolf Lammen, 17-Nov-2013.)
|
|
|
Theorem | anabsan 509 |
Absorption of antecedent with conjunction. (Contributed by NM,
24-Mar-1996.) (Revised by NM, 18-Nov-2013.)
|
|
|
Theorem | anabss1 510 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
|
|
|
Theorem | anabss4 511 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.)
|
|
|
Theorem | anabss5 512 |
Absorption of antecedent into conjunction. (Contributed by NM,
10-May-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
|
|
|
Theorem | anabsi5 513 |
Absorption of antecedent into conjunction. (Contributed by NM,
11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
|
|
|
Theorem | anabsi6 514 |
Absorption of antecedent into conjunction. (Contributed by NM,
14-Aug-2000.)
|
|
|
Theorem | anabsi7 515 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
|
|
|
Theorem | anabsi8 516 |
Absorption of antecedent into conjunction. (Contributed by NM,
26-Sep-1999.)
|
|
|
Theorem | anabss7 517 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 19-Nov-2013.)
|
|
|
Theorem | anabsan2 518 |
Absorption of antecedent with conjunction. (Contributed by NM,
10-May-2004.) (Revised by NM, 1-Jan-2013.)
|
|
|
Theorem | anabss3 519 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
|
|
|
Theorem | an4 520 |
Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
|
|
|
Theorem | an42 521 |
Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
|
|
|
Theorem | an4s 522 |
Inference rearranging 4 conjuncts in antecedent. (Contributed by NM,
10-Aug-1995.)
|
|
|
Theorem | an42s 523 |
Inference rearranging 4 conjuncts in antecedent. (Contributed by NM,
10-Aug-1995.)
|
|
|
Theorem | anandi 524 |
Distribution of conjunction over conjunction. (Contributed by NM,
14-Aug-1995.)
|
|
|
Theorem | anandir 525 |
Distribution of conjunction over conjunction. (Contributed by NM,
24-Aug-1995.)
|
|
|
Theorem | anandis 526 |
Inference that undistributes conjunction in the antecedent.
(Contributed by NM, 7-Jun-2004.)
|
|
|
Theorem | anandirs 527 |
Inference that undistributes conjunction in the antecedent.
(Contributed by NM, 7-Jun-2004.)
|
|
|
Theorem | impbida 528 |
Deduce an equivalence from two implications. (Contributed by NM,
17-Feb-2007.)
|
|
|
Theorem | pm3.45 529 |
Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed
by NM,
3-Jan-2005.)
|
|
|
Theorem | im2anan9 530 |
Deduction joining nested implications to form implication of
conjunctions. (Contributed by NM, 29-Feb-1996.)
|
|
|
Theorem | im2anan9r 531 |
Deduction joining nested implications to form implication of
conjunctions. (Contributed by NM, 29-Feb-1996.)
|
|
|
Theorem | anim12dan 532 |
Conjoin antecedents and consequents in a deduction. (Contributed by
Mario Carneiro, 12-May-2014.)
|
|
|
Theorem | pm5.1 533 |
Two propositions are equivalent if they are both true. Theorem *5.1 of
[WhiteheadRussell] p. 123.
(Contributed by NM, 21-May-1994.)
|
|
|
Theorem | pm3.43 534 |
Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed
by NM,
3-Jan-2005.) (Revised by NM, 27-Nov-2013.)
|
|
|
Theorem | jcab 535 |
Distributive law for implication over conjunction. Compare Theorem *4.76
of [WhiteheadRussell] p. 121.
(Contributed by NM, 3-Apr-1994.) (Proof
shortened by Wolf Lammen, 27-Nov-2013.)
|
|
|
Theorem | pm4.76 536 |
Theorem *4.76 of [WhiteheadRussell] p.
121. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm4.38 537 |
Theorem *4.38 of [WhiteheadRussell] p.
118. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | bi2anan9 538 |
Deduction joining two equivalences to form equivalence of conjunctions.
(Contributed by NM, 31-Jul-1995.)
|
|
|
Theorem | bi2anan9r 539 |
Deduction joining two equivalences to form equivalence of conjunctions.
(Contributed by NM, 19-Feb-1996.)
|
|
|
Theorem | bi2bian9 540 |
Deduction joining two biconditionals with different antecedents.
(Contributed by NM, 12-May-2004.)
|
|
|
Theorem | pm5.33 541 |
Theorem *5.33 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm5.36 542 |
Theorem *5.36 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | bianabs 543 |
Absorb a hypothesis into the second member of a biconditional.
(Contributed by FL, 15-Feb-2007.)
|
|
|
1.2.5 Logical negation
(intuitionistic)
|
|
Axiom | ax-in1 544 |
'Not' introduction. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.)
|
|
|
Axiom | ax-in2 545 |
'Not' elimination. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm2.01 546 |
Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100. This
is valid intuitionistically (in the terminology of Section 1.2 of [Bauer]
p. 482 it is a proof of negation not a proof by contradiction); compare
with pm2.18dc 750 which only holds for some propositions.
(Contributed by
Mario Carneiro, 12-May-2015.)
|
|
|
Theorem | pm2.21 547 |
From a wff and its negation, anything is true. Theorem *2.21 of
[WhiteheadRussell] p. 104. Also
called the Duns Scotus law. (Contributed
by Mario Carneiro, 12-May-2015.)
|
|
|
Theorem | pm2.01d 548 |
Deduction based on reductio ad absurdum. (Contributed by NM,
18-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm2.21d 549 |
A contradiction implies anything. Deduction from pm2.21 547.
(Contributed by NM, 10-Feb-1996.)
|
|
|
Theorem | pm2.21dd 550 |
A contradiction implies anything. Deduction from pm2.21 547.
(Contributed by Mario Carneiro, 9-Feb-2017.)
|
|
|
Theorem | pm2.24 551 |
Theorem *2.24 of [WhiteheadRussell] p.
104. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.24d 552 |
Deduction version of pm2.24 551. (Contributed by NM, 30-Jan-2006.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | pm2.24i 553 |
Inference version of pm2.24 551. (Contributed by NM, 20-Aug-2001.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | con2d 554 |
A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised
by NM, 12-Feb-2013.)
|
|
|
Theorem | mt2d 555 |
Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
|
|
|
Theorem | nsyl3 556 |
A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)
(Revised by NM, 13-Jun-2013.)
|
|
|
Theorem | con2i 557 |
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 558 |
A negated syllogism inference. (Contributed by NM, 31-Dec-1993.)
(Proof shortened by Wolf Lammen, 2-Mar-2013.)
|
|
|
Theorem | notnot 559 |
Double negation introduction. Theorem *2.12 of [WhiteheadRussell] p. 101.
This one holds for all propositions, but its converse only holds for
decidable propositions (see notnotrdc 751). (Contributed by NM,
28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
|
|
|
Theorem | notnotd 560 |
Deduction associated with notnot 559 and notnoti 574. (Contributed by
Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf
Lammen, 27-Mar-2021.)
|
|
|
Theorem | con3d 561 |
A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised
by NM, 31-Jan-2015.)
|
|
|
Theorem | con3i 562 |
A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by Wolf Lammen, 20-Jun-2013.)
|
|
|
Theorem | con3rr3 563 |
Rotate through consequent right. (Contributed by Wolf Lammen,
3-Nov-2013.)
|
|
|
Theorem | con3and 564 |
Variant of con3d 561 with importation. (Contributed by Jonathan
Ben-Naim,
3-Jun-2011.)
|
|
|
Theorem | pm2.01da 565 |
Deduction based on reductio ad absurdum. (Contributed by Mario
Carneiro, 9-Feb-2017.)
|
|
|
Theorem | pm3.2im 566 |
In classical logic, this is just a restatement of pm3.2 126. In
intuitionistic logic, it still holds, but is weaker than pm3.2.
(Contributed by Mario Carneiro, 12-May-2015.)
|
|
|
Theorem | expi 567 |
An exportation inference. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by O'Cat, 28-Nov-2008.)
|
|
|
Theorem | pm2.65i 568 |
Inference rule for proof by contradiction. (Contributed by NM,
18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
|
|
|
Theorem | mt2 569 |
A rule similar to modus tollens. (Contributed by NM, 19-Aug-1993.)
(Proof shortened by Wolf Lammen, 10-Sep-2013.)
|
|
|
Theorem | biijust 570 |
Theorem used to justify definition of intuitionistic biconditional
df-bi 110. (Contributed by NM, 24-Nov-2017.)
|
|
|
Theorem | con3 571 |
Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed
by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Feb-2013.)
|
|
|
Theorem | con2 572 |
Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed
by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
|
|
|
Theorem | mt2i 573 |
Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof
shortened by Wolf Lammen, 15-Sep-2012.)
|
|
|
Theorem | notnoti 574 |
Infer double negation. (Contributed by NM, 27-Feb-2008.)
|
|
|
Theorem | pm2.21i 575 |
A contradiction implies anything. Inference from pm2.21 547.
(Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro,
31-Jan-2015.)
|
|
|
Theorem | pm2.24ii 576 |
A contradiction implies anything. Inference from pm2.24 551.
(Contributed by NM, 27-Feb-2008.)
|
|
|
Theorem | nsyld 577 |
A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.)
|
|
|
Theorem | nsyli 578 |
A negated syllogism inference. (Contributed by NM, 3-May-1994.)
|
|
|
Theorem | mth8 579 |
Theorem 8 of [Margaris] p. 60. (Contributed
by NM, 5-Aug-1993.) (Proof
shortened by Josh Purinton, 29-Dec-2000.)
|
|
|
Theorem | jc 580 |
Inference joining the consequents of two premises. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | pm2.51 581 |
Theorem *2.51 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
|
|
Theorem | pm2.52 582 |
Theorem *2.52 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | expt 583 |
Exportation theorem expressed with primitive connectives. (Contributed by
NM, 5-Aug-1993.)
|
|
|
Theorem | jarl 584 |
Elimination of a nested antecedent. (Contributed by Wolf Lammen,
10-May-2013.)
|
|
|
Theorem | pm2.65 585 |
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 775, are only valid for decidable propositions.
(Contributed by
NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Mar-2013.)
|
|
|
Theorem | pm2.65d 586 |
Deduction rule for proof by contradiction. (Contributed by NM,
26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.)
|
|
|
Theorem | pm2.65da 587 |
Deduction rule for proof by contradiction. (Contributed by NM,
12-Jun-2014.)
|
|
|
Theorem | mto 588 |
The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof
shortened by Wolf Lammen, 11-Sep-2013.)
|
|
|
Theorem | mtod 589 |
Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof
shortened by Wolf Lammen, 11-Sep-2013.)
|
|
|
Theorem | mtoi 590 |
Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof
shortened by Wolf Lammen, 15-Sep-2012.)
|
|
|
Theorem | mtand 591 |
A modus tollens deduction. (Contributed by Jeff Hankins,
19-Aug-2009.)
|
|
|
Theorem | notbid 592 |
Deduction negating both sides of a logical equivalence. (Contributed by
NM, 21-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | con2b 593 |
Contraposition. Bidirectional version of con2 572.
(Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | notbii 594 |
Negate both sides of a logical equivalence. (Contributed by NM,
5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
|
|
Theorem | mtbi 595 |
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 596 |
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 597 |
A deduction from a biconditional, similar to modus tollens.
(Contributed by NM, 26-Nov-1995.)
|
|
|
Theorem | mtbird 598 |
A deduction from a biconditional, similar to modus tollens.
(Contributed by NM, 10-May-1994.)
|
|
|
Theorem | mtbii 599 |
An inference from a biconditional, similar to modus tollens.
(Contributed by NM, 27-Nov-1995.)
|
|
|
Theorem | mtbiri 600 |
An inference from a biconditional, similar to modus tollens.
(Contributed by NM, 24-Aug-1995.)
|
|