Theorem List for Intuitionistic Logic Explorer - 901-1000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 3simpa 901 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | 3simpb 902 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | 3simpc 903 |
Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
(Proof shortened by Andrew Salmon, 13-May-2011.)
|
|
|
Theorem | simp1 904 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | simp2 905 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | simp3 906 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | simpl1 907 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
|
|
Theorem | simpl2 908 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
|
|
Theorem | simpl3 909 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
|
|
Theorem | simpr1 910 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
|
|
Theorem | simpr2 911 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
|
|
Theorem | simpr3 912 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
|
|
Theorem | simp1i 913 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
|
|
Theorem | simp2i 914 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
|
|
Theorem | simp3i 915 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
|
|
Theorem | simp1d 916 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
|
|
Theorem | simp2d 917 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
|
|
Theorem | simp3d 918 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
|
|
Theorem | simp1bi 919 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
|
|
Theorem | simp2bi 920 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
|
|
Theorem | simp3bi 921 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
|
|
Theorem | 3adant1 922 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
|
|
Theorem | 3adant2 923 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
|
|
Theorem | 3adant3 924 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
|
|
Theorem | 3ad2ant1 925 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
|
|
Theorem | 3ad2ant2 926 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
|
|
Theorem | 3ad2ant3 927 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
|
|
Theorem | simp1l 928 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
|
|
Theorem | simp1r 929 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
|
|
Theorem | simp2l 930 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
|
|
Theorem | simp2r 931 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
|
|
Theorem | simp3l 932 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
|
|
Theorem | simp3r 933 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
|
|
Theorem | simp11 934 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp12 935 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp13 936 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp21 937 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp22 938 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp23 939 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp31 940 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp32 941 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp33 942 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simpll1 943 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpll2 944 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpll3 945 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simplr1 946 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simplr2 947 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simplr3 948 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simprl1 949 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simprl2 950 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simprl3 951 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simprr1 952 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simprr2 953 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simprr3 954 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl1l 955 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl1r 956 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl2l 957 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl2r 958 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl3l 959 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl3r 960 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr1l 961 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr1r 962 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr2l 963 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr2r 964 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr3l 965 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr3r 966 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1ll 967 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1lr 968 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1rl 969 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1rr 970 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2ll 971 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2lr 972 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2rl 973 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2rr 974 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3ll 975 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3lr 976 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3rl 977 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3rr 978 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl11 979 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl12 980 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl13 981 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl21 982 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl22 983 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl23 984 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl31 985 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl32 986 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl33 987 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr11 988 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr12 989 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr13 990 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr21 991 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr22 992 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr23 993 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr31 994 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr32 995 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr33 996 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1l1 997 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1l2 998 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1l3 999 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1r1 1000 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|