Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simprr1 | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simprr1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr1 1067 | . 2 | |
2 | 1 | adantl 482 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3a 1037 |
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 386 df-3an 1039 |
This theorem is referenced by: sqrmo 13992 icodiamlt 14174 psgnunilem2 17915 haust1 21156 cnhaus 21158 isreg2 21181 llynlly 21280 restnlly 21285 llyrest 21288 llyidm 21291 nllyidm 21292 cldllycmp 21298 txlly 21439 txnlly 21440 pthaus 21441 txhaus 21450 txkgen 21455 xkohaus 21456 xkococnlem 21462 hauspwpwf1 21791 itg2add 23526 ulmdvlem3 24156 ax5seglem6 25814 fusgrfis 26222 umgr2wlkon 26846 numclwlk1lem2f 27225 numclwwlk5 27246 connpconn 31217 cvmliftmolem2 31264 cvmlift2lem10 31294 cvmlift3lem2 31302 cvmlift3lem8 31308 nosupno 31849 scutbdaybnd 31921 broutsideof3 32233 unblimceq0 32498 paddasslem10 35115 lhpexle2lem 35295 lhpexle3lem 35297 cdlemj3 36111 cdlemkid4 36222 mpaaeu 37720 stoweidlem35 40252 stoweidlem56 40273 stoweidlem59 40276 |
Copyright terms: Public domain | W3C validator |