![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > simp3lr | Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp3lr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplr 732 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant3 980 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem is referenced by: f1oiso2 6039 omeu 6795 tsmsxp 18145 tgqioo 18792 ovolunlem2 19355 plyadd 20097 plymul 20098 coeeu 20105 ntrivcvgmul 25191 btwnconn1lem2 25934 btwnconn1lem3 25935 btwnconn1lem4 25936 pellex 26796 jm2.27 26977 athgt 29950 2llnjN 30061 4atlem12b 30105 lncmp 30277 cdlema2N 30286 cdleme21ct 30823 cdleme24 30846 cdleme27a 30861 cdleme28 30867 cdleme42b 30972 cdlemf 31057 dihlsscpre 31729 dihord4 31753 dihord5apre 31757 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 178 df-an 361 df-3an 938 |
Copyright terms: Public domain | W3C validator |