![]() |
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 1192 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓) | |
2 | 1 | 3ad2antl3 1187 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 |
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 397 df-3an 1089 |
This theorem is referenced by: initoeu2lem2 17898 mulmarep1gsum2 21919 tsmsxp 23502 noinfres 27066 ax5seg 27785 br8d 31427 br8 34221 cgrextend 34582 segconeq 34584 trisegint 34602 ifscgr 34618 cgrsub 34619 btwnxfr 34630 seglecgr12im 34684 segletr 34688 exatleN 37856 atbtwn 37898 3dim1 37919 3dim2 37920 2llnjaN 38018 4atlem10b 38057 4atlem11 38061 4atlem12 38064 2lplnj 38072 cdlemb 38246 paddasslem4 38275 pmodlem1 38298 4atex2 38529 trlval3 38639 arglem1N 38642 cdleme0moN 38677 cdleme17b 38739 cdleme20 38776 cdleme21j 38788 cdleme28c 38824 cdleme35h2 38909 cdleme38n 38916 cdlemg6c 39072 cdlemg6 39075 cdlemg7N 39078 cdlemg11a 39089 cdlemg12e 39099 cdlemg16 39109 cdlemg16ALTN 39110 cdlemg16zz 39112 cdlemg20 39137 cdlemg22 39139 cdlemg37 39141 cdlemg31d 39152 cdlemg29 39157 cdlemg33b 39159 cdlemg33 39163 cdlemg39 39168 cdlemg42 39181 cdlemk25-3 39356 |
Copyright terms: Public domain | W3C validator |