![]() |
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 1189 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓) | |
2 | 1 | 3ad2antl3 1184 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: initoeu2lem2 18037 mulmarep1gsum2 22567 tsmsxp 24150 noinfres 27752 ax5seg 28872 br8d 32530 br8 35578 cgrextend 35832 segconeq 35834 trisegint 35852 ifscgr 35868 cgrsub 35869 btwnxfr 35880 seglecgr12im 35934 segletr 35938 exatleN 39103 atbtwn 39145 3dim1 39166 3dim2 39167 2llnjaN 39265 4atlem10b 39304 4atlem11 39308 4atlem12 39311 2lplnj 39319 cdlemb 39493 paddasslem4 39522 pmodlem1 39545 4atex2 39776 trlval3 39886 arglem1N 39889 cdleme0moN 39924 cdleme17b 39986 cdleme20 40023 cdleme21j 40035 cdleme28c 40071 cdleme35h2 40156 cdleme38n 40163 cdlemg6c 40319 cdlemg6 40322 cdlemg7N 40325 cdlemg11a 40336 cdlemg12e 40346 cdlemg16 40356 cdlemg16ALTN 40357 cdlemg16zz 40359 cdlemg20 40384 cdlemg22 40386 cdlemg37 40388 cdlemg31d 40399 cdlemg29 40404 cdlemg33b 40406 cdlemg33 40410 cdlemg39 40415 cdlemg42 40428 cdlemk25-3 40603 |
Copyright terms: Public domain | W3C validator |