Home | Intuitionistic Logic ExplorerTheorem List (p. 5 of 20)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | mpan2 401 | An inference based on modus ponens. (The proof was shortened by Wolf Lammen, 19-Nov-2012.) |

Theorem | mp2an 402 | An inference based on modus ponens. |

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. |

Theorem | mpand 405 | A deduction based on modus ponens. (The proof was shortened by Wolf Lammen, 7-Apr-2013.) |

Theorem | mpani 406 | An inference based on modus ponens. (The proof was shortened by Wolf Lammen, 19-Nov-2012.) |

Theorem | mpan2i 407 | An inference based on modus ponens. (The proof was shortened by Wolf Lammen, 19-Nov-2012.) |

Theorem | mp2ani 408 | An inference based on modus ponens. |

Theorem | mp2and 409 | A deduction based on modus ponens. |

Theorem | mpanl1 410 | An inference based on modus ponens. (The proof was shortened by Wolf Lammen, 7-Apr-2013.) |

Theorem | mpanl2 411 | An inference based on modus ponens. (The proof was shortened by Andrew Salmon, 7-May-2011.) |

Theorem | mpanl12 412 | An inference based on modus ponens. |

Theorem | mpanr1 413 | An inference based on modus ponens. (The proof was shortened by Andrew Salmon, 7-May-2011.) |

Theorem | mpanr2 414 | An inference based on modus ponens. (The proof was shortened by Andrew Salmon, 7-May-2011.) (The proof was shortened by Wolf Lammen, 7-Apr-2013.) |

Theorem | mpanr2OLD 415 | Obsolete proof of mpanr2 414 as of 7-Apr-2013.) |

Theorem | mpanr12 416 | An inference based on modus ponens. |

Theorem | mpanlr1 417 | An inference based on modus ponens. (The proof was shortened by Wolf Lammen, 7-Apr-2013.) |

Theorem | pm5.74da 418 | Distribution of implication over biconditional (deduction rule). |

Theorem | imdistan 419 | Distribution of implication with conjunction. (The proof was shortened by Wolf Lammen, 6-Dec-2012.) |

Theorem | imdistani 420 | Distribution of implication with conjunction. |

Theorem | imdistanri 421 | Distribution of implication with conjunction. |

Theorem | imdistand 422 | Distribution of implication with conjunction (deduction rule). |

Theorem | imdistanda 423 | Distribution of implication with conjunction (deduction version with conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.) |

Theorem | pm5.32d 424 | Distribution of implication over biconditional (deduction rule). |

Theorem | pm5.32rd 425 | Distribution of implication over biconditional (deduction rule). |

Theorem | pm5.32da 426 | Distribution of implication over biconditional (deduction rule). |

Theorem | pm5.32 427 | Distribution of implication over biconditional. Theorem *5.32 of [WhiteheadRussell] p. 125. |

Theorem | pm5.32i 428 | Distribution of implication over biconditional (inference rule). |

Theorem | pm5.32ri 429 | Distribution of implication over biconditional (inference rule). |

Theorem | biadan2 430 | Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) |

Theorem | anbi2i 431 | Introduce a left conjunct to both sides of a logical equivalence. (The proof was shortened by Wolf Lammen, 16-Nov-2013.) |

Theorem | anbi1i 432 | Introduce a right conjunct to both sides of a logical equivalence. (The proof was shortened by Wolf Lammen, 16-Nov-2013.) |

Theorem | anbi12i 433 | Conjoin both sides of two equivalences. |

Theorem | sylan9bb 434 | Nested syllogism inference conjoining dissimilar antecedents. |

Theorem | sylan9bbr 435 | Nested syllogism inference conjoining dissimilar antecedents. |

Theorem | anbi2d 436 | Deduction adding a left conjunct to both sides of a logical equivalence. (The proof was shortened by Wolf Lammen, 16-Nov-2013.) |

Theorem | anbi1d 437 | Deduction adding a right conjunct to both sides of a logical equivalence. (The proof was shortened by Wolf Lammen, 16-Nov-2013.) |

Theorem | anbi1 438 | Introduce a right conjunct to both sides of a logical equivalence. Theorem *4.36 of [WhiteheadRussell] p. 118. |

Theorem | anbi2 439 | Introduce a left conjunct to both sides of a logical equivalence. |

Theorem | bitr 440 | Theorem *4.22 of [WhiteheadRussell] p. 117. |

Theorem | anbi12d 441 | Deduction joining two equivalences to form equivalence of conjunctions. |

Theorem | pm5.3 442 | Theorem *5.3 of [WhiteheadRussell] p. 125. (The proof was shortened by Andrew Salmon, 7-May-2011.) |

Theorem | adantll 443 | Deduction adding a conjunct to antecedent. (The proof was shortened by Wolf Lammen, 24-Nov-2012.) |

Theorem | adantlr 444 | Deduction adding a conjunct to antecedent. (The proof was shortened by Wolf Lammen, 24-Nov-2012.) |

Theorem | adantrl 445 | Deduction adding a conjunct to antecedent. (The proof was shortened by Wolf Lammen, 24-Nov-2012.) |

Theorem | adantrr 446 | Deduction adding a conjunct to antecedent. (The proof was shortened by Wolf Lammen, 24-Nov-2012.) |

Theorem | adantlll 447 | Deduction adding a conjunct to antecedent. (The proof was shortened by Wolf Lammen, 2-Dec-2012.) |

Theorem | adantllr 448 | Deduction adding a conjunct to antecedent. (The proof was shortened by Wolf Lammen, 4-Dec-2012.) |

Theorem | adantlrl 449 | Deduction adding a conjunct to antecedent. (The proof was shortened by Wolf Lammen, 4-Dec-2012.) |

Theorem | adantlrr 450 | Deduction adding a conjunct to antecedent. (The proof was shortened by Wolf Lammen, 4-Dec-2012.) |

Theorem | adantrll 451 | Deduction adding a conjunct to antecedent. (The proof was shortened by Wolf Lammen, 4-Dec-2012.) |

Theorem | adantrlr 452 | Deduction adding a conjunct to antecedent. (The proof was shortened by Wolf Lammen, 4-Dec-2012.) |

Theorem | adantrrl 453 | Deduction adding a conjunct to antecedent. (The proof was shortened by Wolf Lammen, 4-Dec-2012.) |

Theorem | adantrrr 454 | Deduction adding a conjunct to antecedent. (The proof was shortened by Wolf Lammen, 4-Dec-2012.) |

Theorem | ad2antrr 455 | Deduction adding conjuncts to antecedent. (The proof was shortened by Wolf Lammen, 20-Nov-2012.) |

Theorem | ad3antrrr 456 | Deduction adding 3 conjuncts to antecedent. |

Theorem | ad2antlr 457 | Deduction adding conjuncts to antecedent. (The proof was shortened by Wolf Lammen, 20-Nov-2012.) |

Theorem | ad2antrl 458 | Deduction adding conjuncts to antecedent. |

Theorem | ad2antll 459 | Deduction adding conjuncts to antecedent. |

Theorem | ad2ant2l 460 | Deduction adding two conjuncts to antecedent. |

Theorem | ad2ant2r 461 | Deduction adding two conjuncts to antecedent. |

Theorem | ad2ant2lr 462 | Deduction adding two conjuncts to antecedent. |

Theorem | ad2ant2rl 463 | Deduction adding two conjuncts to antecedent. |

Theorem | simpll 464 | Simplification of a conjunction. |

Theorem | simplr 465 | Simplification of a conjunction. |

Theorem | simprl 466 | Simplification of a conjunction. |

Theorem | simprr 467 | Simplification of a conjunction. |

Theorem | simplll 468 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |

Theorem | simpllr 469 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |

Theorem | simplrl 470 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |

Theorem | simplrr 471 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |

Theorem | simprll 472 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |

Theorem | simprlr 473 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |

Theorem | simprrl 474 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |

Theorem | simprrr 475 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |

Theorem | pm4.87 476 | Theorem *4.87 of [WhiteheadRussell] p. 122. (The proof was shortened by Eric Schmidt, 26-Oct-2006.) |

Theorem | abai 477 | Introduce one conjunct as an antecedent to the other. "abai" stands for "and, biconditional, and, implication". (The proof was shortened by Wolf Lammen, 7-Dec-2012.) |

Theorem | an12 478 | 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. |

Theorem | an32 479 | A rearrangement of conjuncts. (The proof was shortened by Wolf Lammen, 25-Dec-2012.) |

Theorem | an13 480 | A rearrangement of conjuncts. (The proof was shortened by Wolf Lammen, 31-Dec-2012.) |

Theorem | an31 481 | A rearrangement of conjuncts. (The proof was shortened by Wolf Lammen, 31-Dec-2012.) |

Theorem | an12s 482 | Swap two conjuncts in antecedent. The label suffix "s" means that an12 478 is combined with syl 14 (or a variant). |

Theorem | ancom2s 483 | Inference commuting a nested conjunction in antecedent. (The proof was shortened by Wolf Lammen, 24-Nov-2012.) |

Theorem | an13s 484 | Swap two conjuncts in antecedent. |

Theorem | an32s 485 | Swap two conjuncts in antecedent. |

Theorem | ancom1s 486 | Inference commuting a nested conjunction in antecedent. (The proof was shortened by Wolf Lammen, 24-Nov-2012.) |

Theorem | an31s 487 | Swap two conjuncts in antecedent. |

Theorem | anabs1 488 | Absorption into embedded conjunct. (The proof was shortened by Wolf Lammen, 16-Nov-2013.) |

Theorem | anabs5 489 | Absorption into embedded conjunct. (The proof was shortened by Wolf Lammen, 9-Dec-2012.) |

Theorem | anabs7 490 | Absorption into embedded conjunct. (The proof was shortened by Wolf Lammen, 17-Nov-2013.) |

Theorem | anabsan 491 | Absorption of antecedent with conjunction. |

Theorem | anabss1 492 | Absorption of antecedent into conjunction. (The proof was shortened by Wolf Lammen, 31-Dec-2012.) |

Theorem | anabss4 493 | Absorption of antecedent into conjunction. |

Theorem | anabss5 494 | Absorption of antecedent into conjunction. (The proof was shortened by Wolf Lammen, 1-Jan-2013.) |

Theorem | anabsi5 495 | Absorption of antecedent into conjunction. (The proof was shortened by Wolf Lammen, 18-Nov-2013.) |

Theorem | anabsi6 496 | Absorption of antecedent into conjunction. |

Theorem | anabsi7 497 | Absorption of antecedent into conjunction. (The proof was shortened by Wolf Lammen, 18-Nov-2013.) |

Theorem | anabsi8 498 | Absorption of antecedent into conjunction. |

Theorem | anabss7 499 | Absorption of antecedent into conjunction. (The proof was shortened by Wolf Lammen, 19-Nov-2013.) |

Theorem | anabsan2 500 | Absorption of antecedent with conjunction. |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |