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 1184 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓) | |
2 | 1 | 3ad2antl3 1179 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 1081 |
This theorem is referenced by: initoeu2lem2 17263 mulmarep1gsum2 21111 tsmsxp 22690 ax5seg 26651 br8d 30289 br8 32889 cgrextend 33366 segconeq 33368 trisegint 33386 ifscgr 33402 cgrsub 33403 btwnxfr 33414 seglecgr12im 33468 segletr 33472 exatleN 36420 atbtwn 36462 3dim1 36483 3dim2 36484 2llnjaN 36582 4atlem10b 36621 4atlem11 36625 4atlem12 36628 2lplnj 36636 cdlemb 36810 paddasslem4 36839 pmodlem1 36862 4atex2 37093 trlval3 37203 arglem1N 37206 cdleme0moN 37241 cdleme17b 37303 cdleme20 37340 cdleme21j 37352 cdleme28c 37388 cdleme35h2 37473 cdleme38n 37480 cdlemg6c 37636 cdlemg6 37639 cdlemg7N 37642 cdlemg11a 37653 cdlemg12e 37663 cdlemg16 37673 cdlemg16ALTN 37674 cdlemg16zz 37676 cdlemg20 37701 cdlemg22 37703 cdlemg37 37705 cdlemg31d 37716 cdlemg29 37721 cdlemg33b 37723 cdlemg33 37727 cdlemg39 37732 cdlemg42 37745 cdlemk25-3 37920 |
Copyright terms: Public domain | W3C validator |