![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp2ll | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp2ll |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpll 760 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant2 1030 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 189 df-an 373 df-3an 987 |
This theorem is referenced by: tfrlem5 7098 omeu 7286 4sqlem18OLD 14906 4sqlem18 14912 vdwlem10 14940 0catg 15593 mvrf1 18649 mdetuni0 19646 mdetmul 19648 tsmsxp 21169 ax5seglem3 24961 btwnconn1lem1 30854 btwnconn1lem2 30855 btwnconn1lem3 30856 btwnconn1lem12 30865 btwnconn1lem13 30866 lshpkrlem6 32681 athgt 33021 2llnjN 33132 dalaw 33451 lhpmcvr4N 33591 cdlemb2 33606 4atexlemex6 33639 cdlemd7 33770 cdleme01N 33787 cdleme02N 33788 cdleme0ex1N 33789 cdleme0ex2N 33790 cdleme7aa 33808 cdleme7c 33811 cdleme7d 33812 cdleme7e 33813 cdleme7ga 33814 cdleme7 33815 cdleme11a 33826 cdleme20k 33886 cdleme27cl 33933 cdleme42e 34046 cdleme42h 34049 cdleme42i 34050 cdlemf 34130 cdlemg2kq 34169 cdlemg2m 34171 cdlemg8a 34194 cdlemg11aq 34205 cdlemg10c 34206 cdlemg11b 34209 cdlemg17a 34228 cdlemg31b0N 34261 cdlemg31c 34266 cdlemg33c0 34269 cdlemg41 34285 cdlemh2 34383 cdlemn9 34773 dihglbcpreN 34868 dihmeetlem3N 34873 dihmeetlem13N 34887 pellex 35679 expmordi 35795 |
Copyright terms: Public domain | W3C validator |