![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp2rr | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp2rr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprr 766 |
. 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 gruina 9243 4sqlem18OLD 14906 4sqlem18 14912 vdwlem10 14940 mdetuni0 19646 mdetmul 19648 tsmsxp 21169 ax5seglem3 24961 btwnconn1lem1 30854 btwnconn1lem3 30856 btwnconn1lem4 30857 btwnconn1lem5 30858 btwnconn1lem6 30859 btwnconn1lem7 30860 btwnconn1lem12 30865 linethru 30920 2llnjN 33132 2lplnja 33184 2lplnj 33185 cdlemblem 33358 dalaw 33451 pclfinN 33465 lhpmcvr4N 33591 cdlemb2 33606 cdleme01N 33787 cdleme0ex2N 33790 cdleme7c 33811 cdlemefrs29bpre0 33963 cdlemefrs29cpre1 33965 cdlemefrs32fva1 33968 cdlemefs32sn1aw 33981 cdleme41sn3a 34000 cdleme48fv 34066 cdlemk21-2N 34458 dihmeetlem13N 34887 pellex 35679 lmhmfgsplit 35944 iunrelexpmin1 36300 |
Copyright terms: Public domain | W3C validator |