Theorem List for Intuitionistic Logic Explorer - 501-600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | simpllr 501 |
Simplification of a conjunction. (Contributed by Jeff Hankins,
28-Jul-2009.)
|
   
     |
|
Theorem | simplrl 502 |
Simplification of a conjunction. (Contributed by Jeff Hankins,
28-Jul-2009.)
|
     
   |
|
Theorem | simplrr 503 |
Simplification of a conjunction. (Contributed by Jeff Hankins,
28-Jul-2009.)
|
     
   |
|
Theorem | simprll 504 |
Simplification of a conjunction. (Contributed by Jeff Hankins,
28-Jul-2009.)
|
         |
|
Theorem | simprlr 505 |
Simplification of a conjunction. (Contributed by Jeff Hankins,
28-Jul-2009.)
|
         |
|
Theorem | simprrl 506 |
Simplification of a conjunction. (Contributed by Jeff Hankins,
28-Jul-2009.)
|
         |
|
Theorem | simprrr 507 |
Simplification of a conjunction. (Contributed by Jeff Hankins,
28-Jul-2009.)
|
         |
|
Theorem | simp-4l 508 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
           |
|
Theorem | simp-4r 509 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
           |
|
Theorem | simp-5l 510 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
             |
|
Theorem | simp-5r 511 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
             |
|
Theorem | simp-6l 512 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
               |
|
Theorem | simp-6r 513 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
               |
|
Theorem | simp-7l 514 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
       
    
    |
|
Theorem | simp-7r 515 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
       
    
    |
|
Theorem | simp-8l 516 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
                
  |
|
Theorem | simp-8r 517 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
                
  |
|
Theorem | simp-9l 518 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
                 
   |
|
Theorem | simp-9r 519 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
                 
   |
|
Theorem | simp-10l 520 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
                   
   |
|
Theorem | simp-10r 521 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
                   
   |
|
Theorem | simp-11l 522 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
           
    
        |
|
Theorem | simp-11r 523 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
           
    
        |
|
Theorem | pm4.87 524 |
Theorem *4.87 of [WhiteheadRussell] p.
122. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Eric Schmidt, 26-Oct-2006.)
|
        
    
          
          |
|
Theorem | abai 525 |
Introduce one conjunct as an antecedent to the other. "abai" stands
for
"and, biconditional, and, implication". (Contributed by NM,
12-Aug-1993.)
(Proof shortened by Wolf Lammen, 7-Dec-2012.)
|
         |
|
Theorem | an12 526 |
Swap two conjuncts. Note that the first digit (1) in the label refers to
the outer conjunct position, and the next digit (2) to the inner conjunct
position. (Contributed by NM, 12-Mar-1995.)
|
           |
|
Theorem | an32 527 |
A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof
shortened by Wolf Lammen, 25-Dec-2012.)
|
           |
|
Theorem | an13 528 |
A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof
shortened by Wolf Lammen, 31-Dec-2012.)
|
           |
|
Theorem | an31 529 |
A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof
shortened by Wolf Lammen, 31-Dec-2012.)
|
           |
|
Theorem | an12s 530 |
Swap two conjuncts in antecedent. The label suffix "s" means that
an12 526 is combined with syl 14 (or
a variant). (Contributed by NM,
13-Mar-1996.)
|
          
  |
|
Theorem | ancom2s 531 |
Inference commuting a nested conjunction in antecedent. (Contributed by
NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|
             |
|
Theorem | an13s 532 |
Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|
          
  |
|
Theorem | an32s 533 |
Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
|
             |
|
Theorem | ancom1s 534 |
Inference commuting a nested conjunction in antecedent. (Contributed by
NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|
             |
|
Theorem | an31s 535 |
Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|
             |
|
Theorem | anass1rs 536 |
Commutative-associative law for conjunction in an antecedent.
(Contributed by Jeff Madsen, 19-Jun-2011.)
|
             |
|
Theorem | anabs1 537 |
Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995.)
(Proof shortened by Wolf Lammen, 16-Nov-2013.)
|
     
   |
|
Theorem | anabs5 538 |
Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.)
(Proof shortened by Wolf Lammen, 9-Dec-2012.)
|
     
   |
|
Theorem | anabs7 539 |
Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.)
(Proof shortened by Wolf Lammen, 17-Nov-2013.)
|
         |
|
Theorem | anabsan 540 |
Absorption of antecedent with conjunction. (Contributed by NM,
24-Mar-1996.) (Revised by NM, 18-Nov-2013.)
|
   
       |
|
Theorem | anabss1 541 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
|
           |
|
Theorem | anabss4 542 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.)
|
           |
|
Theorem | anabss5 543 |
Absorption of antecedent into conjunction. (Contributed by NM,
10-May-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
|
           |
|
Theorem | anabsi5 544 |
Absorption of antecedent into conjunction. (Contributed by NM,
11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
|
  
        |
|
Theorem | anabsi6 545 |
Absorption of antecedent into conjunction. (Contributed by NM,
14-Aug-2000.)
|
           |
|
Theorem | anabsi7 546 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
|
  
        |
|
Theorem | anabsi8 547 |
Absorption of antecedent into conjunction. (Contributed by NM,
26-Sep-1999.)
|
           |
|
Theorem | anabss7 548 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 19-Nov-2013.)
|
    
  
   |
|
Theorem | anabsan2 549 |
Absorption of antecedent with conjunction. (Contributed by NM,
10-May-2004.) (Revised by NM, 1-Jan-2013.)
|
           |
|
Theorem | anabss3 550 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
|
           |
|
Theorem | an4 551 |
Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
|
               |
|
Theorem | an42 552 |
Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
|
               |
|
Theorem | an4s 553 |
Inference rearranging 4 conjuncts in antecedent. (Contributed by NM,
10-Aug-1995.)
|
                 |
|
Theorem | an42s 554 |
Inference rearranging 4 conjuncts in antecedent. (Contributed by NM,
10-Aug-1995.)
|
                 |
|
Theorem | anandi 555 |
Distribution of conjunction over conjunction. (Contributed by NM,
14-Aug-1995.)
|
             |
|
Theorem | anandir 556 |
Distribution of conjunction over conjunction. (Contributed by NM,
24-Aug-1995.)
|
             |
|
Theorem | anandis 557 |
Inference that undistributes conjunction in the antecedent.
(Contributed by NM, 7-Jun-2004.)
|
               |
|
Theorem | anandirs 558 |
Inference that undistributes conjunction in the antecedent.
(Contributed by NM, 7-Jun-2004.)
|
               |
|
Theorem | syl2an2 559 |
syl2an 283 with antecedents in standard conjunction form.
(Contributed by
Alan Sare, 27-Aug-2016.)
|
               |
|
Theorem | syl2an2r 560 |
syl2anr 284 with antecedents in standard conjunction form.
(Contributed
by Alan Sare, 27-Aug-2016.)
|
   
       
   |
|
Theorem | impbida 561 |
Deduce an equivalence from two implications. (Contributed by NM,
17-Feb-2007.)
|
             |
|
Theorem | pm3.45 562 |
Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed
by NM,
3-Jan-2005.)
|
  
        |
|
Theorem | im2anan9 563 |
Deduction joining nested implications to form implication of
conjunctions. (Contributed by NM, 29-Feb-1996.)
|
                   |
|
Theorem | im2anan9r 564 |
Deduction joining nested implications to form implication of
conjunctions. (Contributed by NM, 29-Feb-1996.)
|
          
        |
|
Theorem | anim12dan 565 |
Conjoin antecedents and consequents in a deduction. (Contributed by
Mario Carneiro, 12-May-2014.)
|
         
       |
|
Theorem | pm5.1 566 |
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 567 |
Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed
by NM,
3-Jan-2005.) (Revised by NM, 27-Nov-2013.)
|
       
     |
|
Theorem | jcab 568 |
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 569 |
Theorem *4.76 of [WhiteheadRussell] p.
121. (Contributed by NM,
3-Jan-2005.)
|
             |
|
Theorem | pm4.38 570 |
Theorem *4.38 of [WhiteheadRussell] p.
118. (Contributed by NM,
3-Jan-2005.)
|
               |
|
Theorem | bi2anan9 571 |
Deduction joining two equivalences to form equivalence of conjunctions.
(Contributed by NM, 31-Jul-1995.)
|
                   |
|
Theorem | bi2anan9r 572 |
Deduction joining two equivalences to form equivalence of conjunctions.
(Contributed by NM, 19-Feb-1996.)
|
          
        |
|
Theorem | bi2bian9 573 |
Deduction joining two biconditionals with different antecedents.
(Contributed by NM, 12-May-2004.)
|
                   |
|
Theorem | pm5.33 574 |
Theorem *5.33 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
       
     |
|
Theorem | pm5.36 575 |
Theorem *5.36 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
           |
|
Theorem | bianabs 576 |
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 577 |
'Not' introduction. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.)
|
  
  |
|
Axiom | ax-in2 578 |
'Not' elimination. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.)
|
     |
|
Theorem | pm2.01 579 |
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 784 which only holds for some propositions.
(Contributed by
Mario Carneiro, 12-May-2015.)
|
  
  |
|
Theorem | pm2.21 580 |
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 581 |
Deduction based on reductio ad absurdum. (Contributed by NM,
18-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
 
     |
|
Theorem | pm2.21d 582 |
A contradiction implies anything. Deduction from pm2.21 580.
(Contributed by NM, 10-Feb-1996.)
|
       |
|
Theorem | pm2.21dd 583 |
A contradiction implies anything. Deduction from pm2.21 580.
(Contributed by Mario Carneiro, 9-Feb-2017.)
|
  
    |
|
Theorem | pm2.24 584 |
Theorem *2.24 of [WhiteheadRussell] p.
104. (Contributed by NM,
3-Jan-2005.)
|
 
   |
|
Theorem | pm2.24d 585 |
Deduction version of pm2.24 584. (Contributed by NM, 30-Jan-2006.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
       |
|
Theorem | pm2.24i 586 |
Inference version of pm2.24 584. (Contributed by NM, 20-Aug-2001.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
   |
|
Theorem | con2d 587 |
A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised
by NM, 12-Feb-2013.)
|
 
   
   |
|
Theorem | mt2d 588 |
Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
|
         |
|
Theorem | nsyl3 589 |
A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)
(Revised by NM, 13-Jun-2013.)
|
    
  |
|
Theorem | con2i 590 |
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 591 |
A negated syllogism inference. (Contributed by NM, 31-Dec-1993.)
(Proof shortened by Wolf Lammen, 2-Mar-2013.)
|
    
  |
|
Theorem | notnot 592 |
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 785). (Contributed by NM,
28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
|
   |
|
Theorem | notnotd 593 |
Deduction associated with notnot 592 and notnoti 607. (Contributed by
Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf
Lammen, 27-Mar-2021.)
|
  
  |
|
Theorem | con3d 594 |
A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised
by NM, 31-Jan-2015.)
|
         |
|
Theorem | con3i 595 |
A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by Wolf Lammen, 20-Jun-2013.)
|
  
  |
|
Theorem | con3rr3 596 |
Rotate through consequent right. (Contributed by Wolf Lammen,
3-Nov-2013.)
|
         |
|
Theorem | con3dimp 597 |
Variant of con3d 594 with importation. (Contributed by Jonathan
Ben-Naim,
3-Jun-2011.)
|
         |
|
Theorem | pm2.01da 598 |
Deduction based on reductio ad absurdum. (Contributed by Mario
Carneiro, 9-Feb-2017.)
|
  
 
  |
|
Theorem | pm3.2im 599 |
In classical logic, this is just a restatement of pm3.2 137. In
intuitionistic logic, it still holds, but is weaker than pm3.2.
(Contributed by Mario Carneiro, 12-May-2015.)
|
 
     |
|
Theorem | expi 600 |
An exportation inference. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by O'Cat, 28-Nov-2008.)
|
         |