| 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 1193 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓) | |
| 2 | 1 | 3ad2antl3 1188 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: initoeu2lem2 18060 mulmarep1gsum2 22580 tsmsxp 24163 noinfres 27767 ax5seg 28953 br8d 32622 br8 35756 cgrextend 36009 segconeq 36011 trisegint 36029 ifscgr 36045 cgrsub 36046 btwnxfr 36057 seglecgr12im 36111 segletr 36115 exatleN 39406 atbtwn 39448 3dim1 39469 3dim2 39470 2llnjaN 39568 4atlem10b 39607 4atlem11 39611 4atlem12 39614 2lplnj 39622 cdlemb 39796 paddasslem4 39825 pmodlem1 39848 4atex2 40079 trlval3 40189 arglem1N 40192 cdleme0moN 40227 cdleme17b 40289 cdleme20 40326 cdleme21j 40338 cdleme28c 40374 cdleme35h2 40459 cdleme38n 40466 cdlemg6c 40622 cdlemg6 40625 cdlemg7N 40628 cdlemg11a 40639 cdlemg12e 40649 cdlemg16 40659 cdlemg16ALTN 40660 cdlemg16zz 40662 cdlemg20 40687 cdlemg22 40689 cdlemg37 40691 cdlemg31d 40702 cdlemg29 40707 cdlemg33b 40709 cdlemg33 40713 cdlemg39 40718 cdlemg42 40731 cdlemk25-3 40906 |
| Copyright terms: Public domain | W3C validator |