![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > simplr1 | Structured version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simplr1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr1 994 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantr 465 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 185 df-an 371 df-3an 967 |
This theorem is referenced by: soltmin 5348 frfi 7671 wemappo 7878 iccsplit 11539 ccatswrd 12472 sqrmo 12863 pcdvdstr 14064 vdwlem12 14175 mreexexlem4d 14708 iscatd2 14742 oppccomfpropd 14789 resssetc 15083 resscatc 15096 mod1ile 15398 mod2ile 15399 prdsmndd 15577 grprcan 15694 prdsrngd 16837 lmodprop2d 17140 lssintcl 17178 prdslmodd 17183 islmhm2 17252 islbs3 17369 ofco2 18469 mdetmul 18571 restopnb 18921 regsep2 19122 iuncon 19174 blsscls2 20221 met2ndci 20239 xrsblre 20530 colline 23204 tglowdim2ln 23206 f1otrg 23296 f1otrge 23297 ax5seglem4 23357 ax5seglem5 23358 axcontlem4 23392 axcontlem8 23396 axcontlem9 23397 axcontlem10 23398 eengtrkg 23410 submomnd 26345 ogrpaddltbi 26354 erdszelem8 27253 btwncomim 28211 btwnswapid 28215 broutsideof3 28324 outsideoftr 28327 outsidele 28330 mendassa 29722 subsubelfzo0 30381 el2wlksotot 30572 rusgranumwlks 30745 extwwlkfablem1 30838 ply1mulgsumlem2 31022 lincresunit3lem2 31169 cvrletrN 33281 ltltncvr 33430 atcvrj2b 33439 2at0mat0 33532 paddasslem11 33837 pmod1i 33855 lautcvr 34099 tendoplass 34790 tendodi1 34791 tendodi2 34792 cdlemk34 34917 |
Copyright terms: Public domain | W3C validator |