Theorem List for Intuitionistic Logic Explorer - 401-500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | syl2ani 401 |
A syllogism inference. (Contributed by NM, 3-Aug-1999.)
|
                 |
|
Theorem | sylan9 402 |
Nested syllogism inference conjoining dissimilar antecedents.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon,
7-May-2011.)
|
               |
|
Theorem | sylan9r 403 |
Nested syllogism inference conjoining dissimilar antecedents.
(Contributed by NM, 5-Aug-1993.)
|
          
    |
|
Theorem | syl2anc 404 |
Syllogism inference combined with contraction. (Contributed by NM,
16-Mar-2012.)
|
           |
|
Theorem | sylancl 405 |
Syllogism inference combined with modus ponens. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
         |
|
Theorem | sylancr 406 |
Syllogism inference combined with modus ponens. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
         |
|
Theorem | sylanblc 407 |
Syllogism inference combined with a biconditional. (Contributed by BJ,
25-Apr-2019.)
|
         |
|
Theorem | sylanblrc 408 |
Syllogism inference combined with a biconditional. (Contributed by BJ,
25-Apr-2019.)
|
         |
|
Theorem | sylanbrc 409 |
Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
           |
|
Theorem | sylancb 410 |
A syllogism inference combined with contraction. (Contributed by NM,
3-Sep-2004.)
|
           |
|
Theorem | sylancbr 411 |
A syllogism inference combined with contraction. (Contributed by NM,
3-Sep-2004.)
|
           |
|
Theorem | sylancom 412 |
Syllogism inference with commutation of antecents. (Contributed by NM,
2-Jul-2008.)
|
         
   |
|
Theorem | mpdan 413 |
An inference based on modus ponens. (Contributed by NM, 23-May-1999.)
(Proof shortened by Wolf Lammen, 22-Nov-2012.)
|
   
     |
|
Theorem | mpancom 414 |
An inference based on modus ponens with commutation of antecedents.
(Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen,
7-Apr-2013.)
|
   
     |
|
Theorem | mpidan 415 |
A deduction which "stacks" a hypothesis. (Contributed by Stanislas
Polu, 9-Mar-2020.) (Proof shortened by Wolf Lammen, 28-Mar-2021.)
|
             |
|
Theorem | mpan 416 |
An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.)
(Proof shortened by Wolf Lammen, 7-Apr-2013.)
|
       |
|
Theorem | mpan2 417 |
An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.)
(Proof shortened by Wolf Lammen, 19-Nov-2012.)
|
       |
|
Theorem | mp2an 418 |
An inference based on modus ponens. (Contributed by NM,
13-Apr-1995.)
|
     |
|
Theorem | mp4an 419 |
An inference based on modus ponens. (Contributed by Jeff Madsen,
15-Jun-2011.)
|
         |
|
Theorem | mpan2d 420 |
A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
|
             |
|
Theorem | mpand 421 |
A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
(Proof shortened by Wolf Lammen, 7-Apr-2013.)
|
             |
|
Theorem | mpani 422 |
An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.)
(Proof shortened by Wolf Lammen, 19-Nov-2012.)
|
       
   |
|
Theorem | mpan2i 423 |
An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.)
(Proof shortened by Wolf Lammen, 19-Nov-2012.)
|
       
   |
|
Theorem | mp2ani 424 |
An inference based on modus ponens. (Contributed by NM,
12-Dec-2004.)
|
         |
|
Theorem | mp2and 425 |
A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
|
             |
|
Theorem | mpanl1 426 |
An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.)
(Proof shortened by Wolf Lammen, 7-Apr-2013.)
|
        
  |
|
Theorem | mpanl2 427 |
An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.)
(Proof shortened by Andrew Salmon, 7-May-2011.)
|
           |
|
Theorem | mpanl12 428 |
An inference based on modus ponens. (Contributed by NM,
13-Jul-2005.)
|
         |
|
Theorem | mpanr1 429 |
An inference based on modus ponens. (Contributed by NM, 3-May-1994.)
(Proof shortened by Andrew Salmon, 7-May-2011.)
|
           |
|
Theorem | mpanr2 430 |
An inference based on modus ponens. (Contributed by NM, 3-May-1994.)
(Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by
Wolf Lammen, 7-Apr-2013.)
|
           |
|
Theorem | mpanr12 431 |
An inference based on modus ponens. (Contributed by NM,
24-Jul-2009.)
|
         |
|
Theorem | mpanlr1 432 |
An inference based on modus ponens. (Contributed by NM, 30-Dec-2004.)
(Proof shortened by Wolf Lammen, 7-Apr-2013.)
|
     
         |
|
Theorem | pm5.74da 433 |
Distribution of implication over biconditional (deduction form).
(Contributed by NM, 4-May-2007.)
|
          
    |
|
Theorem | imdistan 434 |
Distribution of implication with conjunction. (Contributed by NM,
31-May-1999.) (Proof shortened by Wolf Lammen, 6-Dec-2012.)
|
  
          |
|
Theorem | imdistani 435 |
Distribution of implication with conjunction. (Contributed by NM,
1-Aug-1994.)
|
           |
|
Theorem | imdistanri 436 |
Distribution of implication with conjunction. (Contributed by NM,
8-Jan-2002.)
|
           |
|
Theorem | imdistand 437 |
Distribution of implication with conjunction (deduction form).
(Contributed by NM, 27-Aug-2004.)
|
               |
|
Theorem | imdistanda 438 |
Distribution of implication with conjunction (deduction version with
conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.)
|
               |
|
Theorem | pm5.32d 439 |
Distribution of implication over biconditional (deduction form).
(Contributed by NM, 29-Oct-1996.) (Revised by NM, 31-Jan-2015.)
|
      
        |
|
Theorem | pm5.32rd 440 |
Distribution of implication over biconditional (deduction form).
(Contributed by NM, 25-Dec-2004.)
|
      
        |
|
Theorem | pm5.32da 441 |
Distribution of implication over biconditional (deduction form).
(Contributed by NM, 9-Dec-2006.)
|
               |
|
Theorem | pm5.32 442 |
Distribution of implication over biconditional. Theorem *5.32 of
[WhiteheadRussell] p. 125.
(Contributed by NM, 1-Aug-1994.) (Revised by
NM, 31-Jan-2015.)
|
             |
|
Theorem | pm5.32i 443 |
Distribution of implication over biconditional (inference form).
(Contributed by NM, 1-Aug-1994.)
|
           |
|
Theorem | pm5.32ri 444 |
Distribution of implication over biconditional (inference form).
(Contributed by NM, 12-Mar-1995.)
|
           |
|
Theorem | biadan2 445 |
Add a conjunction to an equivalence. (Contributed by Jeff Madsen,
20-Jun-2011.)
|
           |
|
Theorem | anbi2i 446 |
Introduce a left conjunct to both sides of a logical equivalence.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen,
16-Nov-2013.)
|
         |
|
Theorem | anbi1i 447 |
Introduce a right conjunct to both sides of a logical equivalence.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen,
16-Nov-2013.)
|
         |
|
Theorem | anbi2ci 448 |
Variant of anbi2i 446 with commutation. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon,
14-Jun-2011.)
|
         |
|
Theorem | anbi12i 449 |
Conjoin both sides of two equivalences. (Contributed by NM,
5-Aug-1993.)
|
           |
|
Theorem | anbi12ci 450 |
Variant of anbi12i 449 with commutation. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
           |
|
Theorem | sylan9bb 451 |
Nested syllogism inference conjoining dissimilar antecedents.
(Contributed by NM, 4-Mar-1995.)
|
               |
|
Theorem | sylan9bbr 452 |
Nested syllogism inference conjoining dissimilar antecedents.
(Contributed by NM, 4-Mar-1995.)
|
          
    |
|
Theorem | anbi2d 453 |
Deduction adding a left conjunct to both sides of a logical equivalence.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen,
16-Nov-2013.)
|
             |
|
Theorem | anbi1d 454 |
Deduction adding a right conjunct to both sides of a logical
equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf
Lammen, 16-Nov-2013.)
|
             |
|
Theorem | anbi1 455 |
Introduce a right conjunct to both sides of a logical equivalence.
Theorem *4.36 of [WhiteheadRussell] p. 118. (Contributed
by NM,
3-Jan-2005.)
|
    
      |
|
Theorem | anbi2 456 |
Introduce a left conjunct to both sides of a logical equivalence.
(Contributed by NM, 16-Nov-2013.)
|
           |
|
Theorem | bitr 457 |
Theorem *4.22 of [WhiteheadRussell] p.
117. (Contributed by NM,
3-Jan-2005.)
|
           |
|
Theorem | anbi12d 458 |
Deduction joining two equivalences to form equivalence of conjunctions.
(Contributed by NM, 5-Aug-1993.)
|
                 |
|
Theorem | mpan10 459 |
Modus ponens mixed with several conjunctions. (Contributed by Jim
Kingdon, 7-Jan-2018.)
|
           |
|
Theorem | pm5.3 460 |
Theorem *5.3 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|
             |
|
Theorem | adantll 461 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|
       
   |
|
Theorem | adantlr 462 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|
           |
|
Theorem | adantrl 463 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|
           |
|
Theorem | adantrr 464 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|
           |
|
Theorem | adantlll 465 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
26-Dec-2004.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)
|
               |
|
Theorem | adantllr 466 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
|
         
     |
|
Theorem | adantlrl 467 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
|
           
   |
|
Theorem | adantlrr 468 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
|
           
   |
|
Theorem | adantrll 469 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
|
               |
|
Theorem | adantrlr 470 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
|
               |
|
Theorem | adantrrl 471 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
|
               |
|
Theorem | adantrrr 472 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
|
               |
|
Theorem | ad2antrr 473 |
Deduction adding two conjuncts to antecedent. (Contributed by NM,
19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
|
         |
|
Theorem | ad2antlr 474 |
Deduction adding two conjuncts to antecedent. (Contributed by NM,
19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
|
         |
|
Theorem | ad2antrl 475 |
Deduction adding two conjuncts to antecedent. (Contributed by NM,
19-Oct-1999.)
|
         |
|
Theorem | ad2antll 476 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
19-Oct-1999.)
|
         |
|
Theorem | ad3antrrr 477 |
Deduction adding three conjuncts to antecedent. (Contributed by NM,
28-Jul-2012.)
|
           |
|
Theorem | ad3antlr 478 |
Deduction adding three conjuncts to antecedent. (Contributed by Mario
Carneiro, 5-Jan-2017.)
|
           |
|
Theorem | ad4antr 479 |
Deduction adding 4 conjuncts to antecedent. (Contributed by Mario
Carneiro, 4-Jan-2017.)
|
      
      |
|
Theorem | ad4antlr 480 |
Deduction adding 4 conjuncts to antecedent. (Contributed by Mario
Carneiro, 5-Jan-2017.)
|
             |
|
Theorem | ad5antr 481 |
Deduction adding 5 conjuncts to antecedent. (Contributed by Mario
Carneiro, 4-Jan-2017.)
|
               |
|
Theorem | ad5antlr 482 |
Deduction adding 5 conjuncts to antecedent. (Contributed by Mario
Carneiro, 5-Jan-2017.)
|
            
  |
|
Theorem | ad6antr 483 |
Deduction adding 6 conjuncts to antecedent. (Contributed by Mario
Carneiro, 4-Jan-2017.)
|
                 |
|
Theorem | ad6antlr 484 |
Deduction adding 6 conjuncts to antecedent. (Contributed by Mario
Carneiro, 5-Jan-2017.)
|
              
  |
|
Theorem | ad7antr 485 |
Deduction adding 7 conjuncts to antecedent. (Contributed by Mario
Carneiro, 4-Jan-2017.)
|
             
     |
|
Theorem | ad7antlr 486 |
Deduction adding 7 conjuncts to antecedent. (Contributed by Mario
Carneiro, 5-Jan-2017.)
|
             
     |
|
Theorem | ad8antr 487 |
Deduction adding 8 conjuncts to antecedent. (Contributed by Mario
Carneiro, 4-Jan-2017.)
|
          
          |
|
Theorem | ad8antlr 488 |
Deduction adding 8 conjuncts to antecedent. (Contributed by Mario
Carneiro, 5-Jan-2017.)
|
                     |
|
Theorem | ad9antr 489 |
Deduction adding 9 conjuncts to antecedent. (Contributed by Mario
Carneiro, 4-Jan-2017.)
|
                   
   |
|
Theorem | ad9antlr 490 |
Deduction adding 9 conjuncts to antecedent. (Contributed by Mario
Carneiro, 5-Jan-2017.)
|
                       |
|
Theorem | ad10antr 491 |
Deduction adding 10 conjuncts to antecedent. (Contributed by Mario
Carneiro, 4-Jan-2017.)
|
                    
    |
|
Theorem | ad10antlr 492 |
Deduction adding 10 conjuncts to antecedent. (Contributed by Mario
Carneiro, 5-Jan-2017.)
|
                         |
|
Theorem | ad2ant2l 493 |
Deduction adding two conjuncts to antecedent. (Contributed by NM,
8-Jan-2006.)
|
       
     |
|
Theorem | ad2ant2r 494 |
Deduction adding two conjuncts to antecedent. (Contributed by NM,
8-Jan-2006.)
|
             |
|
Theorem | ad2ant2lr 495 |
Deduction adding two conjuncts to antecedent. (Contributed by NM,
23-Nov-2007.)
|
       
     |
|
Theorem | ad2ant2rl 496 |
Deduction adding two conjuncts to antecedent. (Contributed by NM,
24-Nov-2007.)
|
             |
|
Theorem | simpll 497 |
Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
|
       |
|
Theorem | simplr 498 |
Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)
|
       |
|
Theorem | simprl 499 |
Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
|
       |
|
Theorem | simprr 500 |
Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
|
       |