![]() |
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 1190 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) | |
2 | 1 | 3ad2ant3 1128 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1080 |
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 208 df-an 397 df-3an 1082 |
This theorem is referenced by: ps-2c 36214 cdlema1N 36477 trlval3 36873 cdleme12 36957 cdlemednpq 36985 cdleme19d 36992 cdleme19e 36993 cdleme20f 37000 cdleme20h 37002 cdleme20l2 37007 cdleme20l 37008 cdleme20m 37009 cdleme21j 37022 cdleme22a 37026 cdleme22cN 37028 cdleme22f2 37033 cdleme32b 37128 cdlemg12f 37334 cdlemg12g 37335 cdlemg12 37336 cdlemg28a 37379 cdlemg31b0N 37380 cdlemg29 37391 cdlemg33a 37392 cdlemg36 37400 cdlemg42 37415 cdlemk16a 37542 cdlemk21-2N 37577 cdlemk32 37583 cdlemkid2 37610 cdlemk54 37644 cdlemk55a 37645 dihord10 37909 |
Copyright terms: Public domain | W3C validator |