Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simprld | Structured version Visualization version Unicode version |
Description: Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
simprld.1 |
Ref | Expression |
---|---|
simprld |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprld.1 | . . 3 | |
2 | 1 | simprd 479 | . 2 |
3 | 2 | simpld 475 | 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: srglz 18527 lmodvsass 18888 evlssca 19522 dfcgra2 25721 maxsta 31451 lbioc 39739 icccncfext 40100 stoweidlem37 40254 fourierdlem41 40365 fourierdlem48 40371 fourierdlem49 40372 fourierdlem74 40397 fourierdlem75 40398 salgencl 40550 salgenuni 40555 issalgend 40556 smfaddlem1 40971 |
Copyright terms: Public domain | W3C validator |