![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpl31 | 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 |
---|---|
simpl31 | ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl1 1228 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑) | |
2 | 1 | 3ad2antl3 1203 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 |
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 385 df-3an 1074 |
This theorem is referenced by: ax5seglem3a 26009 ax5seg 26017 uhgrwkspth 26861 usgr2wlkspth 26865 br8d 29729 br8 31953 nosupres 32159 cgrextend 32421 segconeq 32423 trisegint 32441 ifscgr 32457 cgrsub 32458 btwnxfr 32469 seglecgr12im 32523 segletr 32527 atbtwn 35235 3dim1 35256 2llnjaN 35355 4atlem10b 35394 4atlem11 35398 4atlem12 35401 2lplnj 35409 paddasslem4 35612 pmodlem1 35635 4atex2 35866 trlval3 35977 arglem1N 35980 cdleme0moN 36015 cdleme17b 36077 cdleme20 36114 cdleme21j 36126 cdleme28c 36162 cdleme35h2 36247 cdlemg6c 36410 cdlemg6 36413 cdlemg7N 36416 cdlemg8c 36419 cdlemg11a 36427 cdlemg11b 36432 cdlemg12e 36437 cdlemg16 36447 cdlemg16ALTN 36448 cdlemg16zz 36450 cdlemg20 36475 cdlemg22 36477 cdlemg37 36479 cdlemg31d 36490 cdlemg33b 36497 cdlemg33 36501 cdlemg39 36506 cdlemg42 36519 cdlemk25-3 36694 cdlemk33N 36699 cdlemk53b 36746 |
Copyright terms: Public domain | W3C validator |