Theorem List for Intuitionistic Logic Explorer - 1001-1100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | simp1ll 1001 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1lr 1002 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1rl 1003 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1rr 1004 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2ll 1005 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2lr 1006 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2rl 1007 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2rr 1008 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3ll 1009 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3lr 1010 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3rl 1011 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3rr 1012 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl11 1013 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl12 1014 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl13 1015 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl21 1016 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl22 1017 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl23 1018 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl31 1019 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl32 1020 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl33 1021 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr11 1022 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr12 1023 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr13 1024 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr21 1025 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr22 1026 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr23 1027 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr31 1028 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr32 1029 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr33 1030 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1l1 1031 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1l2 1032 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1l3 1033 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1r1 1034 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1r2 1035 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1r3 1036 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2l1 1037 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2l2 1038 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2l3 1039 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2r1 1040 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2r2 1041 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2r3 1042 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3l1 1043 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3l2 1044 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3l3 1045 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3r1 1046 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3r2 1047 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3r3 1048 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp11l 1049 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp11r 1050 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp12l 1051 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp12r 1052 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp13l 1053 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp13r 1054 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp21l 1055 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp21r 1056 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp22l 1057 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp22r 1058 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp23l 1059 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp23r 1060 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp31l 1061 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp31r 1062 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp32l 1063 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp32r 1064 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp33l 1065 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp33r 1066 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp111 1067 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp112 1068 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp113 1069 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp121 1070 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp122 1071 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp123 1072 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp131 1073 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp132 1074 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp133 1075 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp211 1076 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp212 1077 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp213 1078 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp221 1079 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp222 1080 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp223 1081 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp231 1082 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp232 1083 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp233 1084 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp311 1085 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp312 1086 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp313 1087 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp321 1088 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp322 1089 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp323 1090 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp331 1091 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp332 1092 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp333 1093 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | 3adantl1 1094 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | 3adantl2 1095 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | 3adantl3 1096 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | 3adantr1 1097 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
27-Apr-2005.)
|
|
|
Theorem | 3adantr2 1098 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
27-Apr-2005.)
|
|
|
Theorem | 3adantr3 1099 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
27-Apr-2005.)
|
|
|
Theorem | 3ad2antl1 1100 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
4-Aug-2007.)
|
|