Home | Metamath
Proof Explorer Theorem List (p. 13 of 466) | < 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-29280) |
Hilbert Space Explorer
(29281-30803) |
Users' Mathboxes
(30804-46521) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | simp3r 1201 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃) | ||
Theorem | simp11 1202 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) | ||
Theorem | simp12 1203 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) | ||
Theorem | simp13 1204 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒) | ||
Theorem | simp21 1205 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simp22 1206 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜒) | ||
Theorem | simp23 1207 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜃) | ||
Theorem | simp31 1208 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜒) | ||
Theorem | simp32 1209 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃) | ||
Theorem | simp33 1210 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏) | ||
Theorem | simpll1 1211 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
Theorem | simpll2 1212 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simpll3 1213 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒) | ||
Theorem | simplr1 1214 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) | ||
Theorem | simplr2 1215 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓) | ||
Theorem | simplr3 1216 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒) | ||
Theorem | simprl1 1217 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) | ||
Theorem | simprl2 1218 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) | ||
Theorem | simprl3 1219 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) | ||
Theorem | simprr1 1220 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
Theorem | simprr2 1221 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
Theorem | simprr3 1222 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
Theorem | simpl1l 1223 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
Theorem | simpl1r 1224 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simpl2l 1225 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
Theorem | simpl2r 1226 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simpl3l 1227 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑) | ||
Theorem | simpl3r 1228 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) | ||
Theorem | simpr1l 1229 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) | ||
Theorem | simpr1r 1230 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) | ||
Theorem | simpr2l 1231 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) | ||
Theorem | simpr2r 1232 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) | ||
Theorem | simpr3l 1233 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) | ||
Theorem | simpr3r 1234 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) | ||
Theorem | simp1ll 1235 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) | ||
Theorem | simp1lr 1236 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) | ||
Theorem | simp1rl 1237 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑) | ||
Theorem | simp1rr 1238 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜓) | ||
Theorem | simp2ll 1239 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑) | ||
Theorem | simp2lr 1240 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓) | ||
Theorem | simp2rl 1241 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑) | ||
Theorem | simp2rr 1242 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) | ||
Theorem | simp3ll 1243 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑) | ||
Theorem | simp3lr 1244 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜓) | ||
Theorem | simp3rl 1245 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜑) | ||
Theorem | simp3rr 1246 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓) | ||
Theorem | simpl11 1247 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜑) | ||
Theorem | simpl12 1248 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓) | ||
Theorem | simpl13 1249 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
Theorem | simpl21 1250 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜑) | ||
Theorem | simpl22 1251 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓) | ||
Theorem | simpl23 1252 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
Theorem | simpl31 1253 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) | ||
Theorem | simpl32 1254 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) | ||
Theorem | simpl33 1255 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒) | ||
Theorem | simpr11 1256 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜑) | ||
Theorem | simpr12 1257 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜓) | ||
Theorem | simpr13 1258 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜒) | ||
Theorem | simpr21 1259 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜑) | ||
Theorem | simpr22 1260 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜓) | ||
Theorem | simpr23 1261 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜒) | ||
Theorem | simpr31 1262 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
Theorem | simpr32 1263 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
Theorem | simpr33 1264 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
Theorem | simp1l1 1265 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
Theorem | simp1l2 1266 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
Theorem | simp1l3 1267 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜒) | ||
Theorem | simp1r1 1268 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
Theorem | simp1r2 1269 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
Theorem | simp1r3 1270 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜒) | ||
Theorem | simp2l1 1271 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜑) | ||
Theorem | simp2l2 1272 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜓) | ||
Theorem | simp2l3 1273 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜒) | ||
Theorem | simp2r1 1274 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) | ||
Theorem | simp2r2 1275 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) | ||
Theorem | simp2r3 1276 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒) | ||
Theorem | simp3l1 1277 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) | ||
Theorem | simp3l2 1278 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) | ||
Theorem | simp3l3 1279 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) | ||
Theorem | simp3r1 1280 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
Theorem | simp3r2 1281 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
Theorem | simp3r3 1282 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
Theorem | simp11l 1283 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
Theorem | simp11r 1284 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
Theorem | simp12l 1285 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
Theorem | simp12r 1286 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
Theorem | simp13l 1287 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
Theorem | simp13r 1288 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
Theorem | simp21l 1289 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜑) | ||
Theorem | simp21r 1290 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜓) | ||
Theorem | simp22l 1291 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜑) | ||
Theorem | simp22r 1292 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓) | ||
Theorem | simp23l 1293 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜑) | ||
Theorem | simp23r 1294 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓) | ||
Theorem | simp31l 1295 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) | ||
Theorem | simp31r 1296 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) | ||
Theorem | simp32l 1297 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) | ||
Theorem | simp32r 1298 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) | ||
Theorem | simp33l 1299 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) | ||
Theorem | simp33r 1300 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |