![]() |
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 397 ∧ w3a 1088 |
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 206 df-an 398 df-3an 1090 |
This theorem is referenced by: ps-2c 38305 cdlema1N 38568 trlval3 38964 cdleme12 39048 cdlemednpq 39076 cdleme19d 39083 cdleme19e 39084 cdleme20f 39091 cdleme20h 39093 cdleme20l2 39098 cdleme20l 39099 cdleme20m 39100 cdleme21j 39113 cdleme22a 39117 cdleme22cN 39119 cdleme22f2 39124 cdleme32b 39219 cdlemg12f 39425 cdlemg12g 39426 cdlemg12 39427 cdlemg28a 39470 cdlemg31b0N 39471 cdlemg29 39482 cdlemg33a 39483 cdlemg36 39491 cdlemg42 39506 cdlemk16a 39633 cdlemk21-2N 39668 cdlemk32 39674 cdlemkid2 39701 cdlemk54 39735 cdlemk55a 39736 dihord10 40000 |
Copyright terms: Public domain | W3C validator |