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