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