![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpl23 | 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 |
---|---|
simpl23 | ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl3 1173 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒) | |
2 | 1 | 3ad2antl2 1166 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 |
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 199 df-an 388 df-3an 1070 |
This theorem is referenced by: mulgdirlem 18045 brbtwn2 26397 ax5seglem3a 26422 ax5seg 26430 axpasch 26433 axeuclid 26455 br8d 30128 br8 32512 frrlem10 32653 nosupbnd2lem1 32736 cgrextend 32990 segconeq 32992 segconeu 32993 trisegint 33010 ifscgr 33026 cgrsub 33027 cgrxfr 33037 lineext 33058 seglecgr12im 33092 segletr 33096 lineunray 33129 lineelsb2 33130 cvrcmp 35864 cvlsupr2 35924 atcvrj2b 36013 atexchcvrN 36021 3atlem3 36066 3atlem5 36068 lplnnle2at 36122 lplnllnneN 36137 4atlem3 36177 4atlem10b 36186 4atlem12 36193 2llnma3r 36369 paddasslem4 36404 paddasslem7 36407 paddasslem8 36408 paddasslem12 36412 paddasslem13 36413 paddasslem15 36415 pmodlem1 36427 pmodlem2 36428 atmod1i1m 36439 llnexchb2lem 36449 4atex2 36658 ltrnatlw 36764 arglem1N 36771 cdlemd4 36782 cdlemd5 36783 cdleme16 36866 cdleme20 36905 cdleme21k 36919 cdleme27N 36950 cdleme28c 36953 cdleme43fsv1snlem 37001 cdleme38n 37045 cdleme40n 37049 cdleme41snaw 37057 cdlemg6c 37201 cdlemg8c 37210 cdlemg8 37212 cdlemg12e 37228 cdlemg16ALTN 37239 cdlemg16zz 37241 cdlemg18a 37259 cdlemg20 37266 cdlemg22 37268 cdlemg37 37270 cdlemg31d 37281 cdlemg33 37292 cdlemg38 37296 cdlemg44b 37313 cdlemk33N 37490 cdlemk34 37491 cdlemk38 37496 cdlemk35s-id 37519 cdlemk39s-id 37521 cdlemk53b 37537 cdlemk53 37538 cdlemk55 37542 cdlemk35u 37545 cdlemk55u 37547 cdleml3N 37559 cdlemn11pre 37791 |
Copyright terms: Public domain | W3C validator |