Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simpr2l | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpr2l |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2l 1087 | . 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: oppccatid 16379 subccatid 16506 setccatid 16734 catccatid 16752 estrccatid 16772 xpccatid 16828 gsmsymgreqlem1 17850 kerf1hrm 18743 nllyidm 21292 ax5seg 25818 3pthdlem1 27024 segconeq 32117 ifscgr 32151 brofs2 32184 brifs2 32185 idinside 32191 btwnconn1lem8 32201 btwnconn1lem12 32205 segcon2 32212 segletr 32221 outsidele 32239 unbdqndv2 32502 lplnexllnN 34850 paddasslem9 35114 pmodlem2 35133 lhp2lt 35287 cdlemc3 35480 cdlemc4 35481 cdlemd1 35485 cdleme3b 35516 cdleme3c 35517 cdleme42ke 35773 cdlemg4c 35900 |
Copyright terms: Public domain | W3C validator |