Home | Metamath
Proof Explorer Theorem List (p. 9 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | simplrr 801 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
Theorem | simprll 802 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
Theorem | simprlr 803 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
Theorem | simprrl 804 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
Theorem | simprrr 805 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
Theorem | simp-4l 806 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-4r 807 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-5l 808 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-5r 809 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-6l 810 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-6r 811 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-7l 812 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-7r 813 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-8l 814 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-8r 815 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-9l 816 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-9r 817 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-10l 818 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-10r 819 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-11l 820 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | simp-11r 821 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | jaob 822 | Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 9-Dec-2012.) |
Theorem | adant423OLD 823 | Obsolete as of 2-Oct-2021. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | jaoian 824 | Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.) |
Theorem | jao1i 825 | Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.) |
Theorem | jaodan 826 | Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.) |
Theorem | mpjaodan 827 | Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination), see natded 27260. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | pm4.77 828 | Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.63 829 | Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.64 830 | Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.61ian 831 | Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.) |
Theorem | pm2.61dan 832 | Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.) |
Theorem | pm2.61ddan 833 | Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.) |
Theorem | pm2.61dda 834 | Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.) |
Theorem | condan 835 | Proof by contradiction. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Wolf Lammen, 19-Jun-2014.) |
Theorem | abai 836 | 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 | pm5.53 837 | Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
Theorem | an12 838 | 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 839 | A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.) |
Theorem | an13 840 | A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.) |
Theorem | an31 841 | A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.) |
Theorem | bianass 842 | An inference to merge two lists of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.) |
Theorem | an12s 843 | Swap two conjuncts in antecedent. The label suffix "s" means that an12 838 is combined with syl 17 (or a variant). (Contributed by NM, 13-Mar-1996.) |
Theorem | ancom2s 844 | Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
Theorem | an13s 845 | Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.) |
Theorem | an32s 846 | Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.) |
Theorem | ancom1s 847 | Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
Theorem | an31s 848 | Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.) |
Theorem | anass1rs 849 | Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.) |
Theorem | anabs1 850 | Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Wolf Lammen, 16-Nov-2013.) |
Theorem | anabs5 851 | Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 9-Dec-2012.) |
Theorem | anabs7 852 | Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 17-Nov-2013.) |
Theorem | a2and 853 | Deduction distributing a conjunction as embedded antecedent. (Contributed by AV, 25-Oct-2019.) (Proof shortened by Wolf Lammen, 19-Jan-2020.) |
Theorem | anabsan 854 | Absorption of antecedent with conjunction. (Contributed by NM, 24-Mar-1996.) |
Theorem | anabss1 855 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 31-Dec-2012.) |
Theorem | anabss4 856 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) |
Theorem | anabss5 857 | Absorption of antecedent into conjunction. (Contributed by NM, 10-May-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2013.) |
Theorem | anabsi5 858 | Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.) |
Theorem | anabsi6 859 | Absorption of antecedent into conjunction. (Contributed by NM, 14-Aug-2000.) |
Theorem | anabsi7 860 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.) |
Theorem | anabsi8 861 | Absorption of antecedent into conjunction. (Contributed by NM, 26-Sep-1999.) |
Theorem | anabss7 862 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 19-Nov-2013.) |
Theorem | anabsan2 863 | Absorption of antecedent with conjunction. (Contributed by NM, 10-May-2004.) |
Theorem | anabss3 864 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.) |
Theorem | an4 865 | Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.) |
Theorem | an42 866 | Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.) |
Theorem | an43 867 | Rearrangement of 4 conjuncts. (Contributed by Rodolfo Medina, 24-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | an3 868 | A rearrangement of conjuncts. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
Theorem | an4s 869 | Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |
Theorem | an42s 870 | Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |
Theorem | anandi 871 | Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.) |
Theorem | anandir 872 | Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.) |
Theorem | anandis 873 | Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.) |
Theorem | anandirs 874 | Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.) |
Theorem | syl2an2 875 | syl2an 494 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) |
Theorem | syl2an2r 876 | syl2anr 495 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) |
Theorem | impbida 877 | Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.) |
Theorem | pm3.48 878 | Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.) |
Theorem | pm3.45 879 | Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |
Theorem | im2anan9 880 | Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.) |
Theorem | im2anan9r 881 | Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.) |
Theorem | anim12dan 882 | Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.) |
Theorem | orim12d 883 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.) |
Theorem | orim1d 884 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
Theorem | orim2d 885 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
Theorem | orim2 886 | Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.38 887 | Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
Theorem | pm2.36 888 | Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
Theorem | pm2.37 889 | Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
Theorem | pm2.73 890 | Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.74 891 | Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Theorem | orimdi 892 | Disjunction distributes over implication. (Contributed by Wolf Lammen, 5-Jan-2013.) |
Theorem | pm2.76 893 | Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.75 894 | Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.) |
Theorem | pm2.8 895 | Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
Theorem | pm2.81 896 | Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.82 897 | Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.85 898 | Theorem *2.85 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
Theorem | pm3.2ni 899 | Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.) |
Theorem | orabs 900 | Absorption of redundant internal disjunct. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 28-Feb-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |