![]() |
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 1231 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒) | |
2 | 1 | 3ad2antl3 1202 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∧ w3a 1071 |
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 197 df-an 383 df-3an 1073 |
This theorem is referenced by: ax5seglem3a 26031 ax5seg 26039 elwwlks2ons3OLD 27103 numclwwlk1lem2foa 27540 br8d 29760 br8 31984 nosupres 32190 cgrextend 32452 segconeq 32454 trisegint 32472 ifscgr 32488 cgrsub 32489 btwnxfr 32500 seglecgr12im 32554 segletr 32558 atbtwn 35254 4atlem10b 35413 4atlem11 35417 4atlem12 35420 2lplnj 35428 paddasslem4 35631 paddasslem7 35634 pmodlem1 35654 4atex2 35885 trlval3 35996 arglem1N 35999 cdleme0moN 36034 cdleme20 36133 cdleme21j 36145 cdleme28c 36181 cdleme38n 36273 cdlemg6c 36429 cdlemg6 36432 cdlemg7N 36435 cdlemg16 36466 cdlemg16ALTN 36467 cdlemg16zz 36469 cdlemg20 36494 cdlemg22 36496 cdlemg37 36498 cdlemg31d 36509 cdlemg29 36514 cdlemg33b 36516 cdlemg33 36520 cdlemg46 36544 cdlemk25-3 36713 |
Copyright terms: Public domain | W3C validator |