![]() |
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 1196 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) | |
2 | 1 | 3ad2ant3 1134 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 1088 |
This theorem is referenced by: ps-2c 39510 cdlema1N 39773 trlval3 40169 cdleme12 40253 cdlemednpq 40281 cdleme19d 40288 cdleme19e 40289 cdleme20f 40296 cdleme20h 40298 cdleme20l2 40303 cdleme20l 40304 cdleme20m 40305 cdleme21j 40318 cdleme22a 40322 cdleme22cN 40324 cdleme22f2 40329 cdleme32b 40424 cdlemg12f 40630 cdlemg12g 40631 cdlemg12 40632 cdlemg28a 40675 cdlemg31b0N 40676 cdlemg29 40687 cdlemg33a 40688 cdlemg36 40696 cdlemg42 40711 cdlemk16a 40838 cdlemk21-2N 40873 cdlemk32 40879 cdlemkid2 40906 cdlemk54 40940 cdlemk55a 40941 dihord10 41205 |
Copyright terms: Public domain | W3C validator |