Home | Metamath
Proof Explorer Theorem List (p. 12 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | simprl3 1101 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) | ||
Theorem | simprr1 1102 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
Theorem | simprr2 1103 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
Theorem | simprr3 1104 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
Theorem | simpl1l 1105 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
Theorem | simpl1r 1106 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simpl2l 1107 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
Theorem | simpl2r 1108 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simpl3l 1109 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑) | ||
Theorem | simpl3r 1110 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) | ||
Theorem | simpr1l 1111 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) | ||
Theorem | simpr1r 1112 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) | ||
Theorem | simpr2l 1113 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) | ||
Theorem | simpr2r 1114 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) | ||
Theorem | simpr3l 1115 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) | ||
Theorem | simpr3r 1116 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) | ||
Theorem | simp1ll 1117 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) | ||
Theorem | simp1lr 1118 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) | ||
Theorem | simp1rl 1119 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑) | ||
Theorem | simp1rr 1120 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜓) | ||
Theorem | simp2ll 1121 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑) | ||
Theorem | simp2lr 1122 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓) | ||
Theorem | simp2rl 1123 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑) | ||
Theorem | simp2rr 1124 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) | ||
Theorem | simp3ll 1125 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑) | ||
Theorem | simp3lr 1126 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜓) | ||
Theorem | simp3rl 1127 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜑) | ||
Theorem | simp3rr 1128 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓) | ||
Theorem | simpl11 1129 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜑) | ||
Theorem | simpl12 1130 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓) | ||
Theorem | simpl13 1131 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
Theorem | simpl21 1132 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜑) | ||
Theorem | simpl22 1133 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓) | ||
Theorem | simpl23 1134 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
Theorem | simpl31 1135 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) | ||
Theorem | simpl32 1136 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) | ||
Theorem | simpl33 1137 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒) | ||
Theorem | simpr11 1138 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜑) | ||
Theorem | simpr12 1139 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜓) | ||
Theorem | simpr13 1140 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜒) | ||
Theorem | simpr21 1141 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜑) | ||
Theorem | simpr22 1142 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜓) | ||
Theorem | simpr23 1143 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜒) | ||
Theorem | simpr31 1144 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
Theorem | simpr32 1145 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
Theorem | simpr33 1146 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
Theorem | simp1l1 1147 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
Theorem | simp1l2 1148 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
Theorem | simp1l3 1149 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜒) | ||
Theorem | simp1r1 1150 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
Theorem | simp1r2 1151 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
Theorem | simp1r3 1152 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜒) | ||
Theorem | simp2l1 1153 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜑) | ||
Theorem | simp2l2 1154 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜓) | ||
Theorem | simp2l3 1155 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜒) | ||
Theorem | simp2r1 1156 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) | ||
Theorem | simp2r2 1157 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) | ||
Theorem | simp2r3 1158 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒) | ||
Theorem | simp3l1 1159 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) | ||
Theorem | simp3l2 1160 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) | ||
Theorem | simp3l3 1161 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) | ||
Theorem | simp3r1 1162 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
Theorem | simp3r2 1163 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
Theorem | simp3r3 1164 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
Theorem | simp11l 1165 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
Theorem | simp11r 1166 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
Theorem | simp12l 1167 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
Theorem | simp12r 1168 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
Theorem | simp13l 1169 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
Theorem | simp13r 1170 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
Theorem | simp21l 1171 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜑) | ||
Theorem | simp21r 1172 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜓) | ||
Theorem | simp22l 1173 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜑) | ||
Theorem | simp22r 1174 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓) | ||
Theorem | simp23l 1175 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜑) | ||
Theorem | simp23r 1176 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓) | ||
Theorem | simp31l 1177 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) | ||
Theorem | simp31r 1178 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) | ||
Theorem | simp32l 1179 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) | ||
Theorem | simp32r 1180 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) | ||
Theorem | simp33l 1181 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) | ||
Theorem | simp33r 1182 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) | ||
Theorem | simp111 1183 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑) | ||
Theorem | simp112 1184 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓) | ||
Theorem | simp113 1185 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒) | ||
Theorem | simp121 1186 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑) | ||
Theorem | simp122 1187 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓) | ||
Theorem | simp123 1188 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒) | ||
Theorem | simp131 1189 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜑) | ||
Theorem | simp132 1190 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜓) | ||
Theorem | simp133 1191 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒) | ||
Theorem | simp211 1192 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜑) | ||
Theorem | simp212 1193 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜓) | ||
Theorem | simp213 1194 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜒) | ||
Theorem | simp221 1195 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜑) | ||
Theorem | simp222 1196 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜓) | ||
Theorem | simp223 1197 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜒) | ||
Theorem | simp231 1198 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜑) | ||
Theorem | simp232 1199 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜓) | ||
Theorem | simp233 1200 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜒) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |