![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpl22 | 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 |
---|---|
simpl22 | ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl2 1192 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓) | |
2 | 1 | 3ad2antl2 1186 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 |
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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: brbtwn2 27683 ax5seg 27716 axpasch 27719 axeuclid 27741 br8d 31358 br8 34145 cgrextend 34531 segconeq 34533 trisegint 34551 ifscgr 34567 cgrsub 34568 cgrxfr 34578 lineext 34599 seglecgr12im 34633 segletr 34637 lineunray 34670 lineelsb2 34671 cvrcmp 37683 cvlatexch3 37738 cvlsupr2 37743 atcvrj2b 37833 atexchcvrN 37841 3dim1 37868 3dim2 37869 3atlem3 37886 3atlem5 37888 lplnnle2at 37942 2llnjaN 37967 4atlem3 37997 4atlem10b 38006 4atlem12 38013 2llnma3r 38189 paddasslem4 38224 paddasslem7 38227 paddasslem8 38228 paddasslem12 38232 paddasslem13 38233 paddasslem15 38235 pmodlem1 38247 pmodlem2 38248 atmod1i1m 38259 llnexchb2lem 38269 4atex2 38478 ltrnatlw 38584 trlval4 38589 arglem1N 38591 cdlemd4 38602 cdlemd5 38603 cdleme0moN 38626 cdleme16 38686 cdleme20 38725 cdleme21k 38739 cdleme27N 38770 cdleme28c 38773 cdleme43fsv1snlem 38821 cdleme38n 38865 cdleme40n 38869 cdleme41snaw 38877 cdlemg6c 39021 cdlemg8c 39030 cdlemg8 39032 cdlemg12e 39048 cdlemg16 39058 cdlemg16ALTN 39059 cdlemg16z 39060 cdlemg16zz 39061 cdlemg18a 39079 cdlemg20 39086 cdlemg22 39088 cdlemg37 39090 cdlemg31d 39101 cdlemg33 39112 cdlemg38 39116 cdlemg44b 39133 cdlemk38 39316 cdlemk35s-id 39339 cdlemk39s-id 39341 cdlemk53b 39357 cdlemk55 39362 cdlemk35u 39365 cdlemk55u 39367 cdlemn11pre 39611 |
Copyright terms: Public domain | W3C validator |