![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > simprr1 | Structured version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simprr1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr1 994 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantl 466 |
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: sqrmo 12845 psgnunilem2 16105 haust1 19074 cnhaus 19076 isreg2 19099 llynlly 19199 restnlly 19204 llyrest 19207 llyidm 19210 nllyidm 19211 cldllycmp 19217 txlly 19327 txnlly 19328 pthaus 19329 txhaus 19338 txkgen 19343 xkohaus 19344 xkococnlem 19350 hauspwpwf1 19678 itg2add 21355 ulmdvlem3 21985 ax5seglem6 23317 conpcon 27260 cvmliftmolem2 27307 cvmlift2lem10 27337 cvmlift3lem2 27345 cvmlift3lem8 27351 broutsideof3 28293 icodiamlt 29301 mpaaeu 29647 stoweidlem35 29970 stoweidlem56 29991 stoweidlem59 29994 frg2woteqm 30792 numclwlk1lem2f 30825 numclwwlk5 30845 paddasslem10 33781 lhpexle2lem 33961 lhpexle3lem 33963 cdlemj3 34775 cdlemkid4 34886 |
Copyright terms: Public domain | W3C validator |