Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simprrd | Structured version Visualization version Unicode version |
Description: Deduction form of simprr 796, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
simprrd.1 |
Ref | Expression |
---|---|
simprrd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprrd.1 | . . 3 | |
2 | 1 | simprd 479 | . 2 |
3 | 2 | simprd 479 | 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: fpwwe2lem3 9455 uzind 11469 latcl2 17048 clatlem 17111 dirge 17237 srgrz 18526 lmodvs1 18891 lmhmsca 19030 evlsvar 19523 mirbtwn 25553 dfcgra2 25721 3trlond 27033 3pthond 27035 3spthond 27037 axtgupdim2OLD 30746 mvtinf 31452 rngoid 33701 rngoideu 33702 rngorn1eq 33733 rngomndo 33734 mzpcl34 37294 icccncfext 40100 fourierdlem12 40336 fourierdlem34 40358 fourierdlem41 40365 fourierdlem48 40371 fourierdlem49 40372 fourierdlem74 40397 fourierdlem75 40398 fourierdlem76 40399 fourierdlem89 40412 fourierdlem91 40414 fourierdlem92 40415 fourierdlem94 40417 fourierdlem113 40436 sssalgen 40553 issalgend 40556 smfaddlem1 40971 |
Copyright terms: Public domain | W3C validator |