Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > anabsan2 | Structured version Visualization version Unicode version |
Description: Absorption of antecedent with conjunction. (Contributed by NM, 10-May-2004.) |
Ref | Expression |
---|---|
anabsan2.1 |
Ref | Expression |
---|---|
anabsan2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anabsan2.1 | . . 3 | |
2 | 1 | an12s 843 | . 2 |
3 | 2 | anabss7 862 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 |
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 |
This theorem is referenced by: anabss3 864 anandirs 874 fvreseq 6319 funcestrcsetclem7 16786 funcsetcestrclem7 16801 lmodvsdi 18886 lmodvsdir 18887 lmodvsass 18888 lss0cl 18947 phlpropd 20000 chpdmatlem3 20645 mbfimasn 23401 slmdvsdi 29768 slmdvsdir 29769 slmdvsass 29770 metider 29937 funcringcsetcALTV2lem7 42042 funcringcsetclem7ALTV 42065 |
Copyright terms: Public domain | W3C validator |