| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simp31l | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| Ref | Expression |
|---|---|
| simp31l | ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simp1l 1198 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) | |
| 2 | 1 | 3ad2ant3 1136 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: ps-2c 39530 cdlema1N 39793 trlval3 40189 cdleme12 40273 cdlemednpq 40301 cdleme19d 40308 cdleme19e 40309 cdleme20f 40316 cdleme20h 40318 cdleme20l2 40323 cdleme20l 40324 cdleme20m 40325 cdleme21j 40338 cdleme22a 40342 cdleme22cN 40344 cdleme22f2 40349 cdleme32b 40444 cdlemg12f 40650 cdlemg12g 40651 cdlemg12 40652 cdlemg28a 40695 cdlemg31b0N 40696 cdlemg29 40707 cdlemg33a 40708 cdlemg36 40716 cdlemg42 40731 cdlemk16a 40858 cdlemk21-2N 40893 cdlemk32 40899 cdlemkid2 40926 cdlemk54 40960 cdlemk55a 40961 dihord10 41225 |
| Copyright terms: Public domain | W3C validator |