Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp3rr | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp3rr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprr 796 | . 2 | |
2 | 1 | 3ad2ant3 1084 | 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: omeu 7665 ntrivcvgmul 14634 tsmsxp 21958 tgqioo 22603 ovolunlem2 23266 plyadd 23973 plymul 23974 coeeu 23981 tghilberti2 25533 cvmlift2lem10 31294 nosupbnd1lem2 31855 btwnconn1lem1 32194 lplnexllnN 34850 2llnjN 34853 4atlem12b 34897 lplncvrlvol2 34901 lncmp 35069 cdlema2N 35078 cdleme11a 35547 cdleme24 35640 cdleme28 35661 cdlemefr29bpre0N 35694 cdlemefr29clN 35695 cdlemefr32fvaN 35697 cdlemefr32fva1 35698 cdlemefs29bpre0N 35704 cdlemefs29bpre1N 35705 cdlemefs29cpre1N 35706 cdlemefs29clN 35707 cdlemefs32fvaN 35710 cdlemefs32fva1 35711 cdleme36m 35749 cdleme17d3 35784 cdlemg36 36002 cdlemj3 36111 cdlemkid1 36210 cdlemk19ylem 36218 cdlemk19xlem 36230 dihlsscpre 36523 dihord4 36547 dihmeetlem1N 36579 dihatlat 36623 jm2.27 37575 |
Copyright terms: Public domain | W3C validator |