![]() |
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 1192 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒) | |
2 | 1 | 3ad2antl3 1186 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 1088 |
This theorem is referenced by: nosupres 27767 noinfres 27782 ax5seglem3a 28960 ax5seg 28968 numclwwlk1lem2foa 30383 br8d 32630 br8 35736 cgrextend 35990 segconeq 35992 trisegint 36010 ifscgr 36026 cgrsub 36027 btwnxfr 36038 seglecgr12im 36092 segletr 36096 atbtwn 39429 4atlem10b 39588 4atlem11 39592 4atlem12 39595 2lplnj 39603 paddasslem4 39806 paddasslem7 39809 pmodlem1 39829 4atex2 40060 trlval3 40170 arglem1N 40173 cdleme0moN 40208 cdleme20 40307 cdleme21j 40319 cdleme28c 40355 cdleme38n 40447 cdlemg6c 40603 cdlemg6 40606 cdlemg7N 40609 cdlemg16 40640 cdlemg16ALTN 40641 cdlemg16zz 40643 cdlemg20 40668 cdlemg22 40670 cdlemg37 40672 cdlemg31d 40683 cdlemg29 40688 cdlemg33b 40690 cdlemg33 40694 cdlemg46 40718 cdlemk25-3 40887 |
Copyright terms: Public domain | W3C validator |