![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > simp1rr | Structured version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp1rr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprr 756 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant1 1009 |
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: f1imass 6079 smo11 6928 zsupss 11048 lsmcv 17337 lspsolvlem 17338 nrmr0reg 19447 plyadd 21811 plymul 21812 coeeu 21819 ax5seglem6 23325 archiabl 26353 sseqval 26908 wsuclem 27899 btwnconn1lem1 28255 btwnconn1lem2 28256 btwnconn1lem12 28266 pellex 29317 mat2pmatghm 31196 mat2pmatmul 31197 lshpsmreu 33063 1cvratlt 33427 llnle 33471 lvolex3N 33491 lnjatN 33733 lncvrat 33735 lncmp 33736 cdlemd6 34156 cdlemk19ylem 34883 |
Copyright terms: Public domain | W3C validator |