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 1185 | . 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: ax5seglem3a 26643 ax5seg 26651 numclwwlk1lem2foa 28060 br8d 30289 br8 32889 nosupres 33104 cgrextend 33366 segconeq 33368 trisegint 33386 ifscgr 33402 cgrsub 33403 btwnxfr 33414 seglecgr12im 33468 segletr 33472 atbtwn 36462 4atlem10b 36621 4atlem11 36625 4atlem12 36628 2lplnj 36636 paddasslem4 36839 paddasslem7 36842 pmodlem1 36862 4atex2 37093 trlval3 37203 arglem1N 37206 cdleme0moN 37241 cdleme20 37340 cdleme21j 37352 cdleme28c 37388 cdleme38n 37480 cdlemg6c 37636 cdlemg6 37639 cdlemg7N 37642 cdlemg16 37673 cdlemg16ALTN 37674 cdlemg16zz 37676 cdlemg20 37701 cdlemg22 37703 cdlemg37 37705 cdlemg31d 37716 cdlemg29 37721 cdlemg33b 37723 cdlemg33 37727 cdlemg46 37751 cdlemk25-3 37920 |
Copyright terms: Public domain | W3C validator |