![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpl33 | 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 |
---|---|
simpl33 | ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl3 1186 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒) | |
2 | 1 | 3ad2antl3 1180 | 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: ax5seglem3a 26399 ax5seg 26407 numclwwlk1lem2foa 27825 br8d 30051 br8 32600 nosupres 32816 cgrextend 33078 segconeq 33080 trisegint 33098 ifscgr 33114 cgrsub 33115 btwnxfr 33126 seglecgr12im 33180 segletr 33184 atbtwn 36113 4atlem10b 36272 4atlem11 36276 4atlem12 36279 2lplnj 36287 paddasslem4 36490 paddasslem7 36493 pmodlem1 36513 4atex2 36744 trlval3 36854 arglem1N 36857 cdleme0moN 36892 cdleme20 36991 cdleme21j 37003 cdleme28c 37039 cdleme38n 37131 cdlemg6c 37287 cdlemg6 37290 cdlemg7N 37293 cdlemg16 37324 cdlemg16ALTN 37325 cdlemg16zz 37327 cdlemg20 37352 cdlemg22 37354 cdlemg37 37356 cdlemg31d 37367 cdlemg29 37372 cdlemg33b 37374 cdlemg33 37378 cdlemg46 37402 cdlemk25-3 37571 |
Copyright terms: Public domain | W3C validator |