![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpl32 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
Ref | Expression |
---|---|
simpl32 | ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl2 1183 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓) | |
2 | 1 | 3ad2antl3 1178 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1078 |
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 1080 |
This theorem is referenced by: initoeu2lem2 17092 mulmarep1gsum2 20855 tsmsxp 22434 ax5seg 26395 br8d 30026 br8 32545 cgrextend 33023 segconeq 33025 trisegint 33043 ifscgr 33059 cgrsub 33060 btwnxfr 33071 seglecgr12im 33125 segletr 33129 exatleN 36021 atbtwn 36063 3dim1 36084 3dim2 36085 2llnjaN 36183 4atlem10b 36222 4atlem11 36226 4atlem12 36229 2lplnj 36237 cdlemb 36411 paddasslem4 36440 pmodlem1 36463 4atex2 36694 trlval3 36804 arglem1N 36807 cdleme0moN 36842 cdleme17b 36904 cdleme20 36941 cdleme21j 36953 cdleme28c 36989 cdleme35h2 37074 cdleme38n 37081 cdlemg6c 37237 cdlemg6 37240 cdlemg7N 37243 cdlemg11a 37254 cdlemg12e 37264 cdlemg16 37274 cdlemg16ALTN 37275 cdlemg16zz 37277 cdlemg20 37302 cdlemg22 37304 cdlemg37 37306 cdlemg31d 37317 cdlemg29 37322 cdlemg33b 37324 cdlemg33 37328 cdlemg39 37333 cdlemg42 37346 cdlemk25-3 37521 |
Copyright terms: Public domain | W3C validator |