![]() |
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 1191 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒) | |
2 | 1 | 3ad2antl2 1184 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 |
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 396 df-3an 1087 |
This theorem is referenced by: frrlem10 8294 mulgdirlem 19053 nosupbnd2lem1 27641 noinfbnd2lem1 27656 brbtwn2 28709 ax5seglem3a 28734 ax5seg 28742 axpasch 28745 axeuclid 28767 br8d 32393 br8 35340 cgrextend 35594 segconeq 35596 segconeu 35597 trisegint 35614 ifscgr 35630 cgrsub 35631 cgrxfr 35641 lineext 35662 seglecgr12im 35696 segletr 35700 lineunray 35733 lineelsb2 35734 cvrcmp 38744 cvlsupr2 38804 atcvrj2b 38894 atexchcvrN 38902 3atlem3 38947 3atlem5 38949 lplnnle2at 39003 lplnllnneN 39018 4atlem3 39058 4atlem10b 39067 4atlem12 39074 2llnma3r 39250 paddasslem4 39285 paddasslem7 39288 paddasslem8 39289 paddasslem12 39293 paddasslem13 39294 paddasslem15 39296 pmodlem1 39308 pmodlem2 39309 atmod1i1m 39320 llnexchb2lem 39330 4atex2 39539 ltrnatlw 39645 arglem1N 39652 cdlemd4 39663 cdlemd5 39664 cdleme16 39747 cdleme20 39786 cdleme21k 39800 cdleme27N 39831 cdleme28c 39834 cdleme43fsv1snlem 39882 cdleme38n 39926 cdleme40n 39930 cdleme41snaw 39938 cdlemg6c 40082 cdlemg8c 40091 cdlemg8 40093 cdlemg12e 40109 cdlemg16ALTN 40120 cdlemg16zz 40122 cdlemg18a 40140 cdlemg20 40147 cdlemg22 40149 cdlemg37 40151 cdlemg31d 40162 cdlemg33 40173 cdlemg38 40177 cdlemg44b 40194 cdlemk33N 40371 cdlemk34 40372 cdlemk38 40377 cdlemk35s-id 40400 cdlemk39s-id 40402 cdlemk53b 40418 cdlemk53 40419 cdlemk55 40423 cdlemk35u 40426 cdlemk55u 40428 cdleml3N 40440 cdlemn11pre 40672 aks6d1c1 41572 |
Copyright terms: Public domain | W3C validator |