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