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 796 | . 2 | |
2 | 1 | 3ad2ant2 1083 | 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: tfrlem5 7476 omeu 7665 gruina 9640 4sqlem18 15666 vdwlem10 15694 mdetuni0 20427 mdetmul 20429 tsmsxp 21958 ax5seglem3 25811 btwnconn1lem1 32194 btwnconn1lem3 32196 btwnconn1lem4 32197 btwnconn1lem5 32198 btwnconn1lem6 32199 btwnconn1lem7 32200 btwnconn1lem12 32205 linethru 32260 2llnjN 34853 2lplnja 34905 2lplnj 34906 cdlemblem 35079 dalaw 35172 pclfinN 35186 lhpmcvr4N 35312 cdlemb2 35327 cdleme01N 35508 cdleme0ex2N 35511 cdleme7c 35532 cdlemefrs29bpre0 35684 cdlemefrs29cpre1 35686 cdlemefrs32fva1 35689 cdlemefs32sn1aw 35702 cdleme41sn3a 35721 cdleme48fv 35787 cdlemk21-2N 36179 dihmeetlem13N 36608 pellex 37399 lmhmfgsplit 37656 iunrelexpmin1 38000 |
Copyright terms: Public domain | W3C validator |