![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > simpr2l | Structured version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpr2l |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2l 1014 |
. 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: oppccatid 14760 subccatid 14858 setccatid 15054 catccatid 15072 xpccatid 15100 gsmsymgreqlem1 16037 kerf1hrm 16937 nllyidm 19209 ax5seg 23319 segconeq 28175 ifscgr 28209 brofs2 28242 brifs2 28243 idinside 28249 btwnconn1lem8 28259 btwnconn1lem12 28263 segcon2 28270 segletr 28279 outsidele 28297 lplnexllnN 33514 paddasslem9 33778 pmodlem2 33797 lhp2lt 33951 cdlemc3 34143 cdlemc4 34144 cdlemd1 34148 cdleme3b 34179 cdleme3c 34180 cdleme42ke 34435 cdlemg4c 34562 |
Copyright terms: Public domain | W3C validator |